open HolKernel boolLib bossLib Parse wordsLib;

(*
  wordsLib.output_words_as_hex();
*)

val _ = new_theory "tables";

val Sbox = Count.apply
 Define
  `Sbox x = case (x:word8) of
      0x0w -> 0x63w:word8
   || 0x1w -> 0x7Cw
   || 0x2w -> 0x77w
   || 0x3w -> 0x7Bw
   || 0x4w -> 0xF2w
   || 0x5w -> 0x6Bw
   || 0x6w -> 0x6Fw
   || 0x7w -> 0xC5w
   || 0x8w -> 0x30w
   || 0x9w -> 0x1w
   || 0xAw -> 0x67w
   || 0xBw -> 0x2Bw
   || 0xCw -> 0xFEw
   || 0xDw -> 0xD7w
   || 0xEw -> 0xABw
   || 0xFw -> 0x76w
   || 0x10w -> 0xCAw
   || 0x11w -> 0x82w
   || 0x12w -> 0xC9w
   || 0x13w -> 0x7Dw
   || 0x14w -> 0xFAw
   || 0x15w -> 0x59w
   || 0x16w -> 0x47w
   || 0x17w -> 0xF0w
   || 0x18w -> 0xADw
   || 0x19w -> 0xD4w
   || 0x1Aw -> 0xA2w
   || 0x1Bw -> 0xAFw
   || 0x1Cw -> 0x9Cw
   || 0x1Dw -> 0xA4w
   || 0x1Ew -> 0x72w
   || 0x1Fw -> 0xC0w
   || 0x20w -> 0xB7w
   || 0x21w -> 0xFDw
   || 0x22w -> 0x93w
   || 0x23w -> 0x26w
   || 0x24w -> 0x36w
   || 0x25w -> 0x3Fw
   || 0x26w -> 0xF7w
   || 0x27w -> 0xCCw
   || 0x28w -> 0x34w
   || 0x29w -> 0xA5w
   || 0x2Aw -> 0xE5w
   || 0x2Bw -> 0xF1w
   || 0x2Cw -> 0x71w
   || 0x2Dw -> 0xD8w
   || 0x2Ew -> 0x31w
   || 0x2Fw -> 0x15w
   || 0x30w -> 0x4w
   || 0x31w -> 0xC7w
   || 0x32w -> 0x23w
   || 0x33w -> 0xC3w
   || 0x34w -> 0x18w
   || 0x35w -> 0x96w
   || 0x36w -> 0x5w
   || 0x37w -> 0x9Aw
   || 0x38w -> 0x7w
   || 0x39w -> 0x12w
   || 0x3Aw -> 0x80w
   || 0x3Bw -> 0xE2w
   || 0x3Cw -> 0xEBw
   || 0x3Dw -> 0x27w
   || 0x3Ew -> 0xB2w
   || 0x3Fw -> 0x75w
   || 0x40w -> 0x9w
   || 0x41w -> 0x83w
   || 0x42w -> 0x2Cw
   || 0x43w -> 0x1Aw
   || 0x44w -> 0x1Bw
   || 0x45w -> 0x6Ew
   || 0x46w -> 0x5Aw
   || 0x47w -> 0xA0w
   || 0x48w -> 0x52w
   || 0x49w -> 0x3Bw
   || 0x4Aw -> 0xD6w
   || 0x4Bw -> 0xB3w
   || 0x4Cw -> 0x29w
   || 0x4Dw -> 0xE3w
   || 0x4Ew -> 0x2Fw
   || 0x4Fw -> 0x84w
   || 0x50w -> 0x53w
   || 0x51w -> 0xD1w
   || 0x52w -> 0x0w
   || 0x53w -> 0xEDw
   || 0x54w -> 0x20w
   || 0x55w -> 0xFCw
   || 0x56w -> 0xB1w
   || 0x57w -> 0x5Bw
   || 0x58w -> 0x6Aw
   || 0x59w -> 0xCBw
   || 0x5Aw -> 0xBEw
   || 0x5Bw -> 0x39w
   || 0x5Cw -> 0x4Aw
   || 0x5Dw -> 0x4Cw
   || 0x5Ew -> 0x58w
   || 0x5Fw -> 0xCFw
   || 0x60w -> 0xD0w
   || 0x61w -> 0xEFw
   || 0x62w -> 0xAAw
   || 0x63w -> 0xFBw
   || 0x64w -> 0x43w
   || 0x65w -> 0x4Dw
   || 0x66w -> 0x33w
   || 0x67w -> 0x85w
   || 0x68w -> 0x45w
   || 0x69w -> 0xF9w
   || 0x6Aw -> 0x2w
   || 0x6Bw -> 0x7Fw
   || 0x6Cw -> 0x50w
   || 0x6Dw -> 0x3Cw
   || 0x6Ew -> 0x9Fw
   || 0x6Fw -> 0xA8w
   || 0x70w -> 0x51w
   || 0x71w -> 0xA3w
   || 0x72w -> 0x40w
   || 0x73w -> 0x8Fw
   || 0x74w -> 0x92w
   || 0x75w -> 0x9Dw
   || 0x76w -> 0x38w
   || 0x77w -> 0xF5w
   || 0x78w -> 0xBCw
   || 0x79w -> 0xB6w
   || 0x7Aw -> 0xDAw
   || 0x7Bw -> 0x21w
   || 0x7Cw -> 0x10w
   || 0x7Dw -> 0xFFw
   || 0x7Ew -> 0xF3w
   || 0x7Fw -> 0xD2w
   || 0x80w -> 0xCDw
   || 0x81w -> 0xCw
   || 0x82w -> 0x13w
   || 0x83w -> 0xECw
   || 0x84w -> 0x5Fw
   || 0x85w -> 0x97w
   || 0x86w -> 0x44w
   || 0x87w -> 0x17w
   || 0x88w -> 0xC4w
   || 0x89w -> 0xA7w
   || 0x8Aw -> 0x7Ew
   || 0x8Bw -> 0x3Dw
   || 0x8Cw -> 0x64w
   || 0x8Dw -> 0x5Dw
   || 0x8Ew -> 0x19w
   || 0x8Fw -> 0x73w
   || 0x90w -> 0x60w
   || 0x91w -> 0x81w
   || 0x92w -> 0x4Fw
   || 0x93w -> 0xDCw
   || 0x94w -> 0x22w
   || 0x95w -> 0x2Aw
   || 0x96w -> 0x90w
   || 0x97w -> 0x88w
   || 0x98w -> 0x46w
   || 0x99w -> 0xEEw
   || 0x9Aw -> 0xB8w
   || 0x9Bw -> 0x14w
   || 0x9Cw -> 0xDEw
   || 0x9Dw -> 0x5Ew
   || 0x9Ew -> 0xBw
   || 0x9Fw -> 0xDBw
   || 0xA0w -> 0xE0w
   || 0xA1w -> 0x32w
   || 0xA2w -> 0x3Aw
   || 0xA3w -> 0xAw
   || 0xA4w -> 0x49w
   || 0xA5w -> 0x6w
   || 0xA6w -> 0x24w
   || 0xA7w -> 0x5Cw
   || 0xA8w -> 0xC2w
   || 0xA9w -> 0xD3w
   || 0xAAw -> 0xACw
   || 0xABw -> 0x62w
   || 0xACw -> 0x91w
   || 0xADw -> 0x95w
   || 0xAEw -> 0xE4w
   || 0xAFw -> 0x79w
   || 0xB0w -> 0xE7w
   || 0xB1w -> 0xC8w
   || 0xB2w -> 0x37w
   || 0xB3w -> 0x6Dw
   || 0xB4w -> 0x8Dw
   || 0xB5w -> 0xD5w
   || 0xB6w -> 0x4Ew
   || 0xB7w -> 0xA9w
   || 0xB8w -> 0x6Cw
   || 0xB9w -> 0x56w
   || 0xBAw -> 0xF4w
   || 0xBBw -> 0xEAw
   || 0xBCw -> 0x65w
   || 0xBDw -> 0x7Aw
   || 0xBEw -> 0xAEw
   || 0xBFw -> 0x8w
   || 0xC0w -> 0xBAw
   || 0xC1w -> 0x78w
   || 0xC2w -> 0x25w
   || 0xC3w -> 0x2Ew
   || 0xC4w -> 0x1Cw
   || 0xC5w -> 0xA6w
   || 0xC6w -> 0xB4w
   || 0xC7w -> 0xC6w
   || 0xC8w -> 0xE8w
   || 0xC9w -> 0xDDw
   || 0xCAw -> 0x74w
   || 0xCBw -> 0x1Fw
   || 0xCCw -> 0x4Bw
   || 0xCDw -> 0xBDw
   || 0xCEw -> 0x8Bw
   || 0xCFw -> 0x8Aw
   || 0xD0w -> 0x70w
   || 0xD1w -> 0x3Ew
   || 0xD2w -> 0xB5w
   || 0xD3w -> 0x66w
   || 0xD4w -> 0x48w
   || 0xD5w -> 0x3w
   || 0xD6w -> 0xF6w
   || 0xD7w -> 0xEw
   || 0xD8w -> 0x61w
   || 0xD9w -> 0x35w
   || 0xDAw -> 0x57w
   || 0xDBw -> 0xB9w
   || 0xDCw -> 0x86w
   || 0xDDw -> 0xC1w
   || 0xDEw -> 0x1Dw
   || 0xDFw -> 0x9Ew
   || 0xE0w -> 0xE1w
   || 0xE1w -> 0xF8w
   || 0xE2w -> 0x98w
   || 0xE3w -> 0x11w
   || 0xE4w -> 0x69w
   || 0xE5w -> 0xD9w
   || 0xE6w -> 0x8Ew
   || 0xE7w -> 0x94w
   || 0xE8w -> 0x9Bw
   || 0xE9w -> 0x1Ew
   || 0xEAw -> 0x87w
   || 0xEBw -> 0xE9w
   || 0xECw -> 0xCEw
   || 0xEDw -> 0x55w
   || 0xEEw -> 0x28w
   || 0xEFw -> 0xDFw
   || 0xF0w -> 0x8Cw
   || 0xF1w -> 0xA1w
   || 0xF2w -> 0x89w
   || 0xF3w -> 0xDw
   || 0xF4w -> 0xBFw
   || 0xF5w -> 0xE6w
   || 0xF6w -> 0x42w
   || 0xF7w -> 0x68w
   || 0xF8w -> 0x41w
   || 0xF9w -> 0x99w
   || 0xFAw -> 0x2Dw
   || 0xFBw -> 0xFw
   || 0xFCw -> 0xB0w
   || 0xFDw -> 0x54w
   || 0xFEw -> 0xBBw
   || 0xFFw -> 0x16w`;

val InvSbox = Count.apply
 Define
  `InvSbox x = case (x:word8) of
      0x0w -> 0x52w:word8
   || 0x1w -> 0x9w
   || 0x2w -> 0x6Aw
   || 0x3w -> 0xD5w
   || 0x4w -> 0x30w
   || 0x5w -> 0x36w
   || 0x6w -> 0xA5w
   || 0x7w -> 0x38w
   || 0x8w -> 0xBFw
   || 0x9w -> 0x40w
   || 0xAw -> 0xA3w
   || 0xBw -> 0x9Ew
   || 0xCw -> 0x81w
   || 0xDw -> 0xF3w
   || 0xEw -> 0xD7w
   || 0xFw -> 0xFBw
   || 0x10w -> 0x7Cw
   || 0x11w -> 0xE3w
   || 0x12w -> 0x39w
   || 0x13w -> 0x82w
   || 0x14w -> 0x9Bw
   || 0x15w -> 0x2Fw
   || 0x16w -> 0xFFw
   || 0x17w -> 0x87w
   || 0x18w -> 0x34w
   || 0x19w -> 0x8Ew
   || 0x1Aw -> 0x43w
   || 0x1Bw -> 0x44w
   || 0x1Cw -> 0xC4w
   || 0x1Dw -> 0xDEw
   || 0x1Ew -> 0xE9w
   || 0x1Fw -> 0xCBw
   || 0x20w -> 0x54w
   || 0x21w -> 0x7Bw
   || 0x22w -> 0x94w
   || 0x23w -> 0x32w
   || 0x24w -> 0xA6w
   || 0x25w -> 0xC2w
   || 0x26w -> 0x23w
   || 0x27w -> 0x3Dw
   || 0x28w -> 0xEEw
   || 0x29w -> 0x4Cw
   || 0x2Aw -> 0x95w
   || 0x2Bw -> 0xBw
   || 0x2Cw -> 0x42w
   || 0x2Dw -> 0xFAw
   || 0x2Ew -> 0xC3w
   || 0x2Fw -> 0x4Ew
   || 0x30w -> 0x8w
   || 0x31w -> 0x2Ew
   || 0x32w -> 0xA1w
   || 0x33w -> 0x66w
   || 0x34w -> 0x28w
   || 0x35w -> 0xD9w
   || 0x36w -> 0x24w
   || 0x37w -> 0xB2w
   || 0x38w -> 0x76w
   || 0x39w -> 0x5Bw
   || 0x3Aw -> 0xA2w
   || 0x3Bw -> 0x49w
   || 0x3Cw -> 0x6Dw
   || 0x3Dw -> 0x8Bw
   || 0x3Ew -> 0xD1w
   || 0x3Fw -> 0x25w
   || 0x40w -> 0x72w
   || 0x41w -> 0xF8w
   || 0x42w -> 0xF6w
   || 0x43w -> 0x64w
   || 0x44w -> 0x86w
   || 0x45w -> 0x68w
   || 0x46w -> 0x98w
   || 0x47w -> 0x16w
   || 0x48w -> 0xD4w
   || 0x49w -> 0xA4w
   || 0x4Aw -> 0x5Cw
   || 0x4Bw -> 0xCCw
   || 0x4Cw -> 0x5Dw
   || 0x4Dw -> 0x65w
   || 0x4Ew -> 0xB6w
   || 0x4Fw -> 0x92w
   || 0x50w -> 0x6Cw
   || 0x51w -> 0x70w
   || 0x52w -> 0x48w
   || 0x53w -> 0x50w
   || 0x54w -> 0xFDw
   || 0x55w -> 0xEDw
   || 0x56w -> 0xB9w
   || 0x57w -> 0xDAw
   || 0x58w -> 0x5Ew
   || 0x59w -> 0x15w
   || 0x5Aw -> 0x46w
   || 0x5Bw -> 0x57w
   || 0x5Cw -> 0xA7w
   || 0x5Dw -> 0x8Dw
   || 0x5Ew -> 0x9Dw
   || 0x5Fw -> 0x84w
   || 0x60w -> 0x90w
   || 0x61w -> 0xD8w
   || 0x62w -> 0xABw
   || 0x63w -> 0x0w
   || 0x64w -> 0x8Cw
   || 0x65w -> 0xBCw
   || 0x66w -> 0xD3w
   || 0x67w -> 0xAw
   || 0x68w -> 0xF7w
   || 0x69w -> 0xE4w
   || 0x6Aw -> 0x58w
   || 0x6Bw -> 0x5w
   || 0x6Cw -> 0xB8w
   || 0x6Dw -> 0xB3w
   || 0x6Ew -> 0x45w
   || 0x6Fw -> 0x6w
   || 0x70w -> 0xD0w
   || 0x71w -> 0x2Cw
   || 0x72w -> 0x1Ew
   || 0x73w -> 0x8Fw
   || 0x74w -> 0xCAw
   || 0x75w -> 0x3Fw
   || 0x76w -> 0xFw
   || 0x77w -> 0x2w
   || 0x78w -> 0xC1w
   || 0x79w -> 0xAFw
   || 0x7Aw -> 0xBDw
   || 0x7Bw -> 0x3w
   || 0x7Cw -> 0x1w
   || 0x7Dw -> 0x13w
   || 0x7Ew -> 0x8Aw
   || 0x7Fw -> 0x6Bw
   || 0x80w -> 0x3Aw
   || 0x81w -> 0x91w
   || 0x82w -> 0x11w
   || 0x83w -> 0x41w
   || 0x84w -> 0x4Fw
   || 0x85w -> 0x67w
   || 0x86w -> 0xDCw
   || 0x87w -> 0xEAw
   || 0x88w -> 0x97w
   || 0x89w -> 0xF2w
   || 0x8Aw -> 0xCFw
   || 0x8Bw -> 0xCEw
   || 0x8Cw -> 0xF0w
   || 0x8Dw -> 0xB4w
   || 0x8Ew -> 0xE6w
   || 0x8Fw -> 0x73w
   || 0x90w -> 0x96w
   || 0x91w -> 0xACw
   || 0x92w -> 0x74w
   || 0x93w -> 0x22w
   || 0x94w -> 0xE7w
   || 0x95w -> 0xADw
   || 0x96w -> 0x35w
   || 0x97w -> 0x85w
   || 0x98w -> 0xE2w
   || 0x99w -> 0xF9w
   || 0x9Aw -> 0x37w
   || 0x9Bw -> 0xE8w
   || 0x9Cw -> 0x1Cw
   || 0x9Dw -> 0x75w
   || 0x9Ew -> 0xDFw
   || 0x9Fw -> 0x6Ew
   || 0xA0w -> 0x47w
   || 0xA1w -> 0xF1w
   || 0xA2w -> 0x1Aw
   || 0xA3w -> 0x71w
   || 0xA4w -> 0x1Dw
   || 0xA5w -> 0x29w
   || 0xA6w -> 0xC5w
   || 0xA7w -> 0x89w
   || 0xA8w -> 0x6Fw
   || 0xA9w -> 0xB7w
   || 0xAAw -> 0x62w
   || 0xABw -> 0xEw
   || 0xACw -> 0xAAw
   || 0xADw -> 0x18w
   || 0xAEw -> 0xBEw
   || 0xAFw -> 0x1Bw
   || 0xB0w -> 0xFCw
   || 0xB1w -> 0x56w
   || 0xB2w -> 0x3Ew
   || 0xB3w -> 0x4Bw
   || 0xB4w -> 0xC6w
   || 0xB5w -> 0xD2w
   || 0xB6w -> 0x79w
   || 0xB7w -> 0x20w
   || 0xB8w -> 0x9Aw
   || 0xB9w -> 0xDBw
   || 0xBAw -> 0xC0w
   || 0xBBw -> 0xFEw
   || 0xBCw -> 0x78w
   || 0xBDw -> 0xCDw
   || 0xBEw -> 0x5Aw
   || 0xBFw -> 0xF4w
   || 0xC0w -> 0x1Fw
   || 0xC1w -> 0xDDw
   || 0xC2w -> 0xA8w
   || 0xC3w -> 0x33w
   || 0xC4w -> 0x88w
   || 0xC5w -> 0x7w
   || 0xC6w -> 0xC7w
   || 0xC7w -> 0x31w
   || 0xC8w -> 0xB1w
   || 0xC9w -> 0x12w
   || 0xCAw -> 0x10w
   || 0xCBw -> 0x59w
   || 0xCCw -> 0x27w
   || 0xCDw -> 0x80w
   || 0xCEw -> 0xECw
   || 0xCFw -> 0x5Fw
   || 0xD0w -> 0x60w
   || 0xD1w -> 0x51w
   || 0xD2w -> 0x7Fw
   || 0xD3w -> 0xA9w
   || 0xD4w -> 0x19w
   || 0xD5w -> 0xB5w
   || 0xD6w -> 0x4Aw
   || 0xD7w -> 0xDw
   || 0xD8w -> 0x2Dw
   || 0xD9w -> 0xE5w
   || 0xDAw -> 0x7Aw
   || 0xDBw -> 0x9Fw
   || 0xDCw -> 0x93w
   || 0xDDw -> 0xC9w
   || 0xDEw -> 0x9Cw
   || 0xDFw -> 0xEFw
   || 0xE0w -> 0xA0w
   || 0xE1w -> 0xE0w
   || 0xE2w -> 0x3Bw
   || 0xE3w -> 0x4Dw
   || 0xE4w -> 0xAEw
   || 0xE5w -> 0x2Aw
   || 0xE6w -> 0xF5w
   || 0xE7w -> 0xB0w
   || 0xE8w -> 0xC8w
   || 0xE9w -> 0xEBw
   || 0xEAw -> 0xBBw
   || 0xEBw -> 0x3Cw
   || 0xECw -> 0x83w
   || 0xEDw -> 0x53w
   || 0xEEw -> 0x99w
   || 0xEFw -> 0x61w
   || 0xF0w -> 0x17w
   || 0xF1w -> 0x2Bw
   || 0xF2w -> 0x4w
   || 0xF3w -> 0x7Ew
   || 0xF4w -> 0xBAw
   || 0xF5w -> 0x77w
   || 0xF6w -> 0xD6w
   || 0xF7w -> 0x26w
   || 0xF8w -> 0xE1w
   || 0xF9w -> 0x69w
   || 0xFAw -> 0x14w
   || 0xFBw -> 0x63w
   || 0xFCw -> 0x55w
   || 0xFDw -> 0x21w
   || 0xFEw -> 0xCw
   || 0xFFw -> 0x7Dw`;

val LESS_THM =
  CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM;

val Sbox_Inversion = Q.store_thm
("Sbox_Inversion",
 `!w:word8. InvSbox (Sbox w) = w`,
 Cases THEN FULL_SIMP_TAC std_ss [wordsTheory.dimword_8, LESS_THM]
   THEN EVAL_TAC);

(*  The following has been superseded by the construction
    of tables in MultScript. We'll keep it for info purposes.

val GF256_by_2 = Count.apply word8Define
  `(GF256_by_2 0x0w = 0x0w) /\
   (GF256_by_2 0x1w = 0x2w) /\
   (GF256_by_2 0x2w = 0x4w) /\
   (GF256_by_2 0x3w = 0x6w) /\
   (GF256_by_2 0x4w = 0x8w) /\
   (GF256_by_2 0x5w = 0xAw) /\
   (GF256_by_2 0x6w = 0xCw) /\
   (GF256_by_2 0x7w = 0xEw) /\
   (GF256_by_2 0x8w = 0x10w) /\
   (GF256_by_2 0x9w = 0x12w) /\
   (GF256_by_2 0xAw = 0x14w) /\
   (GF256_by_2 0xBw = 0x16w) /\
   (GF256_by_2 0xCw = 0x18w) /\
   (GF256_by_2 0xDw = 0x1Aw) /\
   (GF256_by_2 0xEw = 0x1Cw) /\
   (GF256_by_2 0xFw = 0x1Ew) /\
   (GF256_by_2 0x10w = 0x20w) /\
   (GF256_by_2 0x11w = 0x22w) /\
   (GF256_by_2 0x12w = 0x24w) /\
   (GF256_by_2 0x13w = 0x26w) /\
   (GF256_by_2 0x14w = 0x28w) /\
   (GF256_by_2 0x15w = 0x2Aw) /\
   (GF256_by_2 0x16w = 0x2Cw) /\
   (GF256_by_2 0x17w = 0x2Ew) /\
   (GF256_by_2 0x18w = 0x30w) /\
   (GF256_by_2 0x19w = 0x32w) /\
   (GF256_by_2 0x1Aw = 0x34w) /\
   (GF256_by_2 0x1Bw = 0x36w) /\
   (GF256_by_2 0x1Cw = 0x38w) /\
   (GF256_by_2 0x1Dw = 0x3Aw) /\
   (GF256_by_2 0x1Ew = 0x3Cw) /\
   (GF256_by_2 0x1Fw = 0x3Ew) /\
   (GF256_by_2 0x20w = 0x40w) /\
   (GF256_by_2 0x21w = 0x42w) /\
   (GF256_by_2 0x22w = 0x44w) /\
   (GF256_by_2 0x23w = 0x46w) /\
   (GF256_by_2 0x24w = 0x48w) /\
   (GF256_by_2 0x25w = 0x4Aw) /\
   (GF256_by_2 0x26w = 0x4Cw) /\
   (GF256_by_2 0x27w = 0x4Ew) /\
   (GF256_by_2 0x28w = 0x50w) /\
   (GF256_by_2 0x29w = 0x52w) /\
   (GF256_by_2 0x2Aw = 0x54w) /\
   (GF256_by_2 0x2Bw = 0x56w) /\
   (GF256_by_2 0x2Cw = 0x58w) /\
   (GF256_by_2 0x2Dw = 0x5Aw) /\
   (GF256_by_2 0x2Ew = 0x5Cw) /\
   (GF256_by_2 0x2Fw = 0x5Ew) /\
   (GF256_by_2 0x30w = 0x60w) /\
   (GF256_by_2 0x31w = 0x62w) /\
   (GF256_by_2 0x32w = 0x64w) /\
   (GF256_by_2 0x33w = 0x66w) /\
   (GF256_by_2 0x34w = 0x68w) /\
   (GF256_by_2 0x35w = 0x6Aw) /\
   (GF256_by_2 0x36w = 0x6Cw) /\
   (GF256_by_2 0x37w = 0x6Ew) /\
   (GF256_by_2 0x38w = 0x70w) /\
   (GF256_by_2 0x39w = 0x72w) /\
   (GF256_by_2 0x3Aw = 0x74w) /\
   (GF256_by_2 0x3Bw = 0x76w) /\
   (GF256_by_2 0x3Cw = 0x78w) /\
   (GF256_by_2 0x3Dw = 0x7Aw) /\
   (GF256_by_2 0x3Ew = 0x7Cw) /\
   (GF256_by_2 0x3Fw = 0x7Ew) /\
   (GF256_by_2 0x40w = 0x80w) /\
   (GF256_by_2 0x41w = 0x82w) /\
   (GF256_by_2 0x42w = 0x84w) /\
   (GF256_by_2 0x43w = 0x86w) /\
   (GF256_by_2 0x44w = 0x88w) /\
   (GF256_by_2 0x45w = 0x8Aw) /\
   (GF256_by_2 0x46w = 0x8Cw) /\
   (GF256_by_2 0x47w = 0x8Ew) /\
   (GF256_by_2 0x48w = 0x90w) /\
   (GF256_by_2 0x49w = 0x92w) /\
   (GF256_by_2 0x4Aw = 0x94w) /\
   (GF256_by_2 0x4Bw = 0x96w) /\
   (GF256_by_2 0x4Cw = 0x98w) /\
   (GF256_by_2 0x4Dw = 0x9Aw) /\
   (GF256_by_2 0x4Ew = 0x9Cw) /\
   (GF256_by_2 0x4Fw = 0x9Ew) /\
   (GF256_by_2 0x50w = 0xA0w) /\
   (GF256_by_2 0x51w = 0xA2w) /\
   (GF256_by_2 0x52w = 0xA4w) /\
   (GF256_by_2 0x53w = 0xA6w) /\
   (GF256_by_2 0x54w = 0xA8w) /\
   (GF256_by_2 0x55w = 0xAAw) /\
   (GF256_by_2 0x56w = 0xACw) /\
   (GF256_by_2 0x57w = 0xAEw) /\
   (GF256_by_2 0x58w = 0xB0w) /\
   (GF256_by_2 0x59w = 0xB2w) /\
   (GF256_by_2 0x5Aw = 0xB4w) /\
   (GF256_by_2 0x5Bw = 0xB6w) /\
   (GF256_by_2 0x5Cw = 0xB8w) /\
   (GF256_by_2 0x5Dw = 0xBAw) /\
   (GF256_by_2 0x5Ew = 0xBCw) /\
   (GF256_by_2 0x5Fw = 0xBEw) /\
   (GF256_by_2 0x60w = 0xC0w) /\
   (GF256_by_2 0x61w = 0xC2w) /\
   (GF256_by_2 0x62w = 0xC4w) /\
   (GF256_by_2 0x63w = 0xC6w) /\
   (GF256_by_2 0x64w = 0xC8w) /\
   (GF256_by_2 0x65w = 0xCAw) /\
   (GF256_by_2 0x66w = 0xCCw) /\
   (GF256_by_2 0x67w = 0xCEw) /\
   (GF256_by_2 0x68w = 0xD0w) /\
   (GF256_by_2 0x69w = 0xD2w) /\
   (GF256_by_2 0x6Aw = 0xD4w) /\
   (GF256_by_2 0x6Bw = 0xD6w) /\
   (GF256_by_2 0x6Cw = 0xD8w) /\
   (GF256_by_2 0x6Dw = 0xDAw) /\
   (GF256_by_2 0x6Ew = 0xDCw) /\
   (GF256_by_2 0x6Fw = 0xDEw) /\
   (GF256_by_2 0x70w = 0xE0w) /\
   (GF256_by_2 0x71w = 0xE2w) /\
   (GF256_by_2 0x72w = 0xE4w) /\
   (GF256_by_2 0x73w = 0xE6w) /\
   (GF256_by_2 0x74w = 0xE8w) /\
   (GF256_by_2 0x75w = 0xEAw) /\
   (GF256_by_2 0x76w = 0xECw) /\
   (GF256_by_2 0x77w = 0xEEw) /\
   (GF256_by_2 0x78w = 0xF0w) /\
   (GF256_by_2 0x79w = 0xF2w) /\
   (GF256_by_2 0x7Aw = 0xF4w) /\
   (GF256_by_2 0x7Bw = 0xF6w) /\
   (GF256_by_2 0x7Cw = 0xF8w) /\
   (GF256_by_2 0x7Dw = 0xFAw) /\
   (GF256_by_2 0x7Ew = 0xFCw) /\
   (GF256_by_2 0x7Fw = 0xFEw) /\
   (GF256_by_2 0x80w = 0x1Bw) /\
   (GF256_by_2 0x81w = 0x19w) /\
   (GF256_by_2 0x82w = 0x1Fw) /\
   (GF256_by_2 0x83w = 0x1Dw) /\
   (GF256_by_2 0x84w = 0x13w) /\
   (GF256_by_2 0x85w = 0x11w) /\
   (GF256_by_2 0x86w = 0x17w) /\
   (GF256_by_2 0x87w = 0x15w) /\
   (GF256_by_2 0x88w = 0xBw)  /\
   (GF256_by_2 0x89w = 0x9w)  /\
   (GF256_by_2 0x8Aw = 0xFw)  /\
   (GF256_by_2 0x8Bw = 0xDw)  /\
   (GF256_by_2 0x8Cw = 0x3w)  /\
   (GF256_by_2 0x8Dw = 0x1w)  /\
   (GF256_by_2 0x8Ew = 0x7w)  /\
   (GF256_by_2 0x8Fw = 0x5w)  /\
   (GF256_by_2 0x90w = 0x3Bw) /\
   (GF256_by_2 0x91w = 0x39w) /\
   (GF256_by_2 0x92w = 0x3Fw) /\
   (GF256_by_2 0x93w = 0x3Dw) /\
   (GF256_by_2 0x94w = 0x33w) /\
   (GF256_by_2 0x95w = 0x31w) /\
   (GF256_by_2 0x96w = 0x37w) /\
   (GF256_by_2 0x97w = 0x35w) /\
   (GF256_by_2 0x98w = 0x2Bw) /\
   (GF256_by_2 0x99w = 0x29w) /\
   (GF256_by_2 0x9Aw = 0x2Fw) /\
   (GF256_by_2 0x9Bw = 0x2Dw) /\
   (GF256_by_2 0x9Cw = 0x23w) /\
   (GF256_by_2 0x9Dw = 0x21w) /\
   (GF256_by_2 0x9Ew = 0x27w) /\
   (GF256_by_2 0x9Fw = 0x25w) /\
   (GF256_by_2 0xA0w = 0x5Bw) /\
   (GF256_by_2 0xA1w = 0x59w) /\
   (GF256_by_2 0xA2w = 0x5Fw) /\
   (GF256_by_2 0xA3w = 0x5Dw) /\
   (GF256_by_2 0xA4w = 0x53w) /\
   (GF256_by_2 0xA5w = 0x51w) /\
   (GF256_by_2 0xA6w = 0x57w) /\
   (GF256_by_2 0xA7w = 0x55w) /\
   (GF256_by_2 0xA8w = 0x4Bw) /\
   (GF256_by_2 0xA9w = 0x49w) /\
   (GF256_by_2 0xAAw = 0x4Fw) /\
   (GF256_by_2 0xABw = 0x4Dw) /\
   (GF256_by_2 0xACw = 0x43w) /\
   (GF256_by_2 0xADw = 0x41w) /\
   (GF256_by_2 0xAEw = 0x47w) /\
   (GF256_by_2 0xAFw = 0x45w) /\
   (GF256_by_2 0xB0w = 0x7Bw) /\
   (GF256_by_2 0xB1w = 0x79w) /\
   (GF256_by_2 0xB2w = 0x7Fw) /\
   (GF256_by_2 0xB3w = 0x7Dw) /\
   (GF256_by_2 0xB4w = 0x73w) /\
   (GF256_by_2 0xB5w = 0x71w) /\
   (GF256_by_2 0xB6w = 0x77w) /\
   (GF256_by_2 0xB7w = 0x75w) /\
   (GF256_by_2 0xB8w = 0x6Bw) /\
   (GF256_by_2 0xB9w = 0x69w) /\
   (GF256_by_2 0xBAw = 0x6Fw) /\
   (GF256_by_2 0xBBw = 0x6Dw) /\
   (GF256_by_2 0xBCw = 0x63w) /\
   (GF256_by_2 0xBDw = 0x61w) /\
   (GF256_by_2 0xBEw = 0x67w) /\
   (GF256_by_2 0xBFw = 0x65w) /\
   (GF256_by_2 0xC0w = 0x9Bw) /\
   (GF256_by_2 0xC1w = 0x99w) /\
   (GF256_by_2 0xC2w = 0x9Fw) /\
   (GF256_by_2 0xC3w = 0x9Dw) /\
   (GF256_by_2 0xC4w = 0x93w) /\
   (GF256_by_2 0xC5w = 0x91w) /\
   (GF256_by_2 0xC6w = 0x97w) /\
   (GF256_by_2 0xC7w = 0x95w) /\
   (GF256_by_2 0xC8w = 0x8Bw) /\
   (GF256_by_2 0xC9w = 0x89w) /\
   (GF256_by_2 0xCAw = 0x8Fw) /\
   (GF256_by_2 0xCBw = 0x8Dw) /\
   (GF256_by_2 0xCCw = 0x83w) /\
   (GF256_by_2 0xCDw = 0x81w) /\
   (GF256_by_2 0xCEw = 0x87w) /\
   (GF256_by_2 0xCFw = 0x85w) /\
   (GF256_by_2 0xD0w = 0xBBw) /\
   (GF256_by_2 0xD1w = 0xB9w) /\
   (GF256_by_2 0xD2w = 0xBFw) /\
   (GF256_by_2 0xD3w = 0xBDw) /\
   (GF256_by_2 0xD4w = 0xB3w) /\
   (GF256_by_2 0xD5w = 0xB1w) /\
   (GF256_by_2 0xD6w = 0xB7w) /\
   (GF256_by_2 0xD7w = 0xB5w) /\
   (GF256_by_2 0xD8w = 0xABw) /\
   (GF256_by_2 0xD9w = 0xA9w) /\
   (GF256_by_2 0xDAw = 0xAFw) /\
   (GF256_by_2 0xDBw = 0xADw) /\
   (GF256_by_2 0xDCw = 0xA3w) /\
   (GF256_by_2 0xDDw = 0xA1w) /\
   (GF256_by_2 0xDEw = 0xA7w) /\
   (GF256_by_2 0xDFw = 0xA5w) /\
   (GF256_by_2 0xE0w = 0xDBw) /\
   (GF256_by_2 0xE1w = 0xD9w) /\
   (GF256_by_2 0xE2w = 0xDFw) /\
   (GF256_by_2 0xE3w = 0xDDw) /\
   (GF256_by_2 0xE4w = 0xD3w) /\
   (GF256_by_2 0xE5w = 0xD1w) /\
   (GF256_by_2 0xE6w = 0xD7w) /\
   (GF256_by_2 0xE7w = 0xD5w) /\
   (GF256_by_2 0xE8w = 0xCBw) /\
   (GF256_by_2 0xE9w = 0xC9w) /\
   (GF256_by_2 0xEAw = 0xCFw) /\
   (GF256_by_2 0xEBw = 0xCDw) /\
   (GF256_by_2 0xECw = 0xC3w) /\
   (GF256_by_2 0xEDw = 0xC1w) /\
   (GF256_by_2 0xEEw = 0xC7w) /\
   (GF256_by_2 0xEFw = 0xC5w) /\
   (GF256_by_2 0xF0w = 0xFBw) /\
   (GF256_by_2 0xF1w = 0xF9w) /\
   (GF256_by_2 0xF2w = 0xFFw) /\
   (GF256_by_2 0xF3w = 0xFDw) /\
   (GF256_by_2 0xF4w = 0xF3w) /\
   (GF256_by_2 0xF5w = 0xF1w) /\
   (GF256_by_2 0xF6w = 0xF7w) /\
   (GF256_by_2 0xF7w = 0xF5w) /\
   (GF256_by_2 0xF8w = 0xEBw) /\
   (GF256_by_2 0xF9w = 0xE9w) /\
   (GF256_by_2 0xFAw = 0xEFw) /\
   (GF256_by_2 0xFBw = 0xEDw) /\
   (GF256_by_2 0xFCw = 0xE3w) /\
   (GF256_by_2 0xFDw = 0xE1w) /\
   (GF256_by_2 0xFEw = 0xE7w) /\
   (GF256_by_2 0xFFw = 0xE5w)`;

val GF256_by_3 = Count.apply word8Define
  `(GF256_by_3 0x0w = 0x0w) /\
   (GF256_by_3 0x1w = 0x3w) /\
   (GF256_by_3 0x2w = 0x6w) /\
   (GF256_by_3 0x3w = 0x5w) /\
   (GF256_by_3 0x4w = 0xCw) /\
   (GF256_by_3 0x5w = 0xFw) /\
   (GF256_by_3 0x6w = 0xAw) /\
   (GF256_by_3 0x7w = 0x9w) /\
   (GF256_by_3 0x8w = 0x18w) /\
   (GF256_by_3 0x9w = 0x1Bw) /\
   (GF256_by_3 0xAw = 0x1Ew) /\
   (GF256_by_3 0xBw = 0x1Dw) /\
   (GF256_by_3 0xCw = 0x14w) /\
   (GF256_by_3 0xDw = 0x17w) /\
   (GF256_by_3 0xEw = 0x12w) /\
   (GF256_by_3 0xFw = 0x11w) /\
   (GF256_by_3 0x10w = 0x30w) /\
   (GF256_by_3 0x11w = 0x33w) /\
   (GF256_by_3 0x12w = 0x36w) /\
   (GF256_by_3 0x13w = 0x35w) /\
   (GF256_by_3 0x14w = 0x3Cw) /\
   (GF256_by_3 0x15w = 0x3Fw) /\
   (GF256_by_3 0x16w = 0x3Aw) /\
   (GF256_by_3 0x17w = 0x39w) /\
   (GF256_by_3 0x18w = 0x28w) /\
   (GF256_by_3 0x19w = 0x2Bw) /\
   (GF256_by_3 0x1Aw = 0x2Ew) /\
   (GF256_by_3 0x1Bw = 0x2Dw) /\
   (GF256_by_3 0x1Cw = 0x24w) /\
   (GF256_by_3 0x1Dw = 0x27w) /\
   (GF256_by_3 0x1Ew = 0x22w) /\
   (GF256_by_3 0x1Fw = 0x21w) /\
   (GF256_by_3 0x20w = 0x60w) /\
   (GF256_by_3 0x21w = 0x63w) /\
   (GF256_by_3 0x22w = 0x66w) /\
   (GF256_by_3 0x23w = 0x65w) /\
   (GF256_by_3 0x24w = 0x6Cw) /\
   (GF256_by_3 0x25w = 0x6Fw) /\
   (GF256_by_3 0x26w = 0x6Aw) /\
   (GF256_by_3 0x27w = 0x69w) /\
   (GF256_by_3 0x28w = 0x78w) /\
   (GF256_by_3 0x29w = 0x7Bw) /\
   (GF256_by_3 0x2Aw = 0x7Ew) /\
   (GF256_by_3 0x2Bw = 0x7Dw) /\
   (GF256_by_3 0x2Cw = 0x74w) /\
   (GF256_by_3 0x2Dw = 0x77w) /\
   (GF256_by_3 0x2Ew = 0x72w) /\
   (GF256_by_3 0x2Fw = 0x71w) /\
   (GF256_by_3 0x30w = 0x50w) /\
   (GF256_by_3 0x31w = 0x53w) /\
   (GF256_by_3 0x32w = 0x56w) /\
   (GF256_by_3 0x33w = 0x55w) /\
   (GF256_by_3 0x34w = 0x5Cw) /\
   (GF256_by_3 0x35w = 0x5Fw) /\
   (GF256_by_3 0x36w = 0x5Aw) /\
   (GF256_by_3 0x37w = 0x59w) /\
   (GF256_by_3 0x38w = 0x48w) /\
   (GF256_by_3 0x39w = 0x4Bw) /\
   (GF256_by_3 0x3Aw = 0x4Ew) /\
   (GF256_by_3 0x3Bw = 0x4Dw) /\
   (GF256_by_3 0x3Cw = 0x44w) /\
   (GF256_by_3 0x3Dw = 0x47w) /\
   (GF256_by_3 0x3Ew = 0x42w) /\
   (GF256_by_3 0x3Fw = 0x41w) /\
   (GF256_by_3 0x40w = 0xC0w) /\
   (GF256_by_3 0x41w = 0xC3w) /\
   (GF256_by_3 0x42w = 0xC6w) /\
   (GF256_by_3 0x43w = 0xC5w) /\
   (GF256_by_3 0x44w = 0xCCw) /\
   (GF256_by_3 0x45w = 0xCFw) /\
   (GF256_by_3 0x46w = 0xCAw) /\
   (GF256_by_3 0x47w = 0xC9w) /\
   (GF256_by_3 0x48w = 0xD8w) /\
   (GF256_by_3 0x49w = 0xDBw) /\
   (GF256_by_3 0x4Aw = 0xDEw) /\
   (GF256_by_3 0x4Bw = 0xDDw) /\
   (GF256_by_3 0x4Cw = 0xD4w) /\
   (GF256_by_3 0x4Dw = 0xD7w) /\
   (GF256_by_3 0x4Ew = 0xD2w) /\
   (GF256_by_3 0x4Fw = 0xD1w) /\
   (GF256_by_3 0x50w = 0xF0w) /\
   (GF256_by_3 0x51w = 0xF3w) /\
   (GF256_by_3 0x52w = 0xF6w) /\
   (GF256_by_3 0x53w = 0xF5w) /\
   (GF256_by_3 0x54w = 0xFCw) /\
   (GF256_by_3 0x55w = 0xFFw) /\
   (GF256_by_3 0x56w = 0xFAw) /\
   (GF256_by_3 0x57w = 0xF9w) /\
   (GF256_by_3 0x58w = 0xE8w) /\
   (GF256_by_3 0x59w = 0xEBw) /\
   (GF256_by_3 0x5Aw = 0xEEw) /\
   (GF256_by_3 0x5Bw = 0xEDw) /\
   (GF256_by_3 0x5Cw = 0xE4w) /\
   (GF256_by_3 0x5Dw = 0xE7w) /\
   (GF256_by_3 0x5Ew = 0xE2w) /\
   (GF256_by_3 0x5Fw = 0xE1w) /\
   (GF256_by_3 0x60w = 0xA0w) /\
   (GF256_by_3 0x61w = 0xA3w) /\
   (GF256_by_3 0x62w = 0xA6w) /\
   (GF256_by_3 0x63w = 0xA5w) /\
   (GF256_by_3 0x64w = 0xACw) /\
   (GF256_by_3 0x65w = 0xAFw) /\
   (GF256_by_3 0x66w = 0xAAw) /\
   (GF256_by_3 0x67w = 0xA9w) /\
   (GF256_by_3 0x68w = 0xB8w) /\
   (GF256_by_3 0x69w = 0xBBw) /\
   (GF256_by_3 0x6Aw = 0xBEw) /\
   (GF256_by_3 0x6Bw = 0xBDw) /\
   (GF256_by_3 0x6Cw = 0xB4w) /\
   (GF256_by_3 0x6Dw = 0xB7w) /\
   (GF256_by_3 0x6Ew = 0xB2w) /\
   (GF256_by_3 0x6Fw = 0xB1w) /\
   (GF256_by_3 0x70w = 0x90w) /\
   (GF256_by_3 0x71w = 0x93w) /\
   (GF256_by_3 0x72w = 0x96w) /\
   (GF256_by_3 0x73w = 0x95w) /\
   (GF256_by_3 0x74w = 0x9Cw) /\
   (GF256_by_3 0x75w = 0x9Fw) /\
   (GF256_by_3 0x76w = 0x9Aw) /\
   (GF256_by_3 0x77w = 0x99w) /\
   (GF256_by_3 0x78w = 0x88w) /\
   (GF256_by_3 0x79w = 0x8Bw) /\
   (GF256_by_3 0x7Aw = 0x8Ew) /\
   (GF256_by_3 0x7Bw = 0x8Dw) /\
   (GF256_by_3 0x7Cw = 0x84w) /\
   (GF256_by_3 0x7Dw = 0x87w) /\
   (GF256_by_3 0x7Ew = 0x82w) /\
   (GF256_by_3 0x7Fw = 0x81w) /\
   (GF256_by_3 0x80w = 0x9Bw) /\
   (GF256_by_3 0x81w = 0x98w) /\
   (GF256_by_3 0x82w = 0x9Dw) /\
   (GF256_by_3 0x83w = 0x9Ew) /\
   (GF256_by_3 0x84w = 0x97w) /\
   (GF256_by_3 0x85w = 0x94w) /\
   (GF256_by_3 0x86w = 0x91w) /\
   (GF256_by_3 0x87w = 0x92w) /\
   (GF256_by_3 0x88w = 0x83w) /\
   (GF256_by_3 0x89w = 0x80w) /\
   (GF256_by_3 0x8Aw = 0x85w) /\
   (GF256_by_3 0x8Bw = 0x86w) /\
   (GF256_by_3 0x8Cw = 0x8Fw) /\
   (GF256_by_3 0x8Dw = 0x8Cw) /\
   (GF256_by_3 0x8Ew = 0x89w) /\
   (GF256_by_3 0x8Fw = 0x8Aw) /\
   (GF256_by_3 0x90w = 0xABw) /\
   (GF256_by_3 0x91w = 0xA8w) /\
   (GF256_by_3 0x92w = 0xADw) /\
   (GF256_by_3 0x93w = 0xAEw) /\
   (GF256_by_3 0x94w = 0xA7w) /\
   (GF256_by_3 0x95w = 0xA4w) /\
   (GF256_by_3 0x96w = 0xA1w) /\
   (GF256_by_3 0x97w = 0xA2w) /\
   (GF256_by_3 0x98w = 0xB3w) /\
   (GF256_by_3 0x99w = 0xB0w) /\
   (GF256_by_3 0x9Aw = 0xB5w) /\
   (GF256_by_3 0x9Bw = 0xB6w) /\
   (GF256_by_3 0x9Cw = 0xBFw) /\
   (GF256_by_3 0x9Dw = 0xBCw) /\
   (GF256_by_3 0x9Ew = 0xB9w) /\
   (GF256_by_3 0x9Fw = 0xBAw) /\
   (GF256_by_3 0xA0w = 0xFBw) /\
   (GF256_by_3 0xA1w = 0xF8w) /\
   (GF256_by_3 0xA2w = 0xFDw) /\
   (GF256_by_3 0xA3w = 0xFEw) /\
   (GF256_by_3 0xA4w = 0xF7w) /\
   (GF256_by_3 0xA5w = 0xF4w) /\
   (GF256_by_3 0xA6w = 0xF1w) /\
   (GF256_by_3 0xA7w = 0xF2w) /\
   (GF256_by_3 0xA8w = 0xE3w) /\
   (GF256_by_3 0xA9w = 0xE0w) /\
   (GF256_by_3 0xAAw = 0xE5w) /\
   (GF256_by_3 0xABw = 0xE6w) /\
   (GF256_by_3 0xACw = 0xEFw) /\
   (GF256_by_3 0xADw = 0xECw) /\
   (GF256_by_3 0xAEw = 0xE9w) /\
   (GF256_by_3 0xAFw = 0xEAw) /\
   (GF256_by_3 0xB0w = 0xCBw) /\
   (GF256_by_3 0xB1w = 0xC8w) /\
   (GF256_by_3 0xB2w = 0xCDw) /\
   (GF256_by_3 0xB3w = 0xCEw) /\
   (GF256_by_3 0xB4w = 0xC7w) /\
   (GF256_by_3 0xB5w = 0xC4w) /\
   (GF256_by_3 0xB6w = 0xC1w) /\
   (GF256_by_3 0xB7w = 0xC2w) /\
   (GF256_by_3 0xB8w = 0xD3w) /\
   (GF256_by_3 0xB9w = 0xD0w) /\
   (GF256_by_3 0xBAw = 0xD5w) /\
   (GF256_by_3 0xBBw = 0xD6w) /\
   (GF256_by_3 0xBCw = 0xDFw) /\
   (GF256_by_3 0xBDw = 0xDCw) /\
   (GF256_by_3 0xBEw = 0xD9w) /\
   (GF256_by_3 0xBFw = 0xDAw) /\
   (GF256_by_3 0xC0w = 0x5Bw) /\
   (GF256_by_3 0xC1w = 0x58w) /\
   (GF256_by_3 0xC2w = 0x5Dw) /\
   (GF256_by_3 0xC3w = 0x5Ew) /\
   (GF256_by_3 0xC4w = 0x57w) /\
   (GF256_by_3 0xC5w = 0x54w) /\
   (GF256_by_3 0xC6w = 0x51w) /\
   (GF256_by_3 0xC7w = 0x52w) /\
   (GF256_by_3 0xC8w = 0x43w) /\
   (GF256_by_3 0xC9w = 0x40w) /\
   (GF256_by_3 0xCAw = 0x45w) /\
   (GF256_by_3 0xCBw = 0x46w) /\
   (GF256_by_3 0xCCw = 0x4Fw) /\
   (GF256_by_3 0xCDw = 0x4Cw) /\
   (GF256_by_3 0xCEw = 0x49w) /\
   (GF256_by_3 0xCFw = 0x4Aw) /\
   (GF256_by_3 0xD0w = 0x6Bw) /\
   (GF256_by_3 0xD1w = 0x68w) /\
   (GF256_by_3 0xD2w = 0x6Dw) /\
   (GF256_by_3 0xD3w = 0x6Ew) /\
   (GF256_by_3 0xD4w = 0x67w) /\
   (GF256_by_3 0xD5w = 0x64w) /\
   (GF256_by_3 0xD6w = 0x61w) /\
   (GF256_by_3 0xD7w = 0x62w) /\
   (GF256_by_3 0xD8w = 0x73w) /\
   (GF256_by_3 0xD9w = 0x70w) /\
   (GF256_by_3 0xDAw = 0x75w) /\
   (GF256_by_3 0xDBw = 0x76w) /\
   (GF256_by_3 0xDCw = 0x7Fw) /\
   (GF256_by_3 0xDDw = 0x7Cw) /\
   (GF256_by_3 0xDEw = 0x79w) /\
   (GF256_by_3 0xDFw = 0x7Aw) /\
   (GF256_by_3 0xE0w = 0x3Bw) /\
   (GF256_by_3 0xE1w = 0x38w) /\
   (GF256_by_3 0xE2w = 0x3Dw) /\
   (GF256_by_3 0xE3w = 0x3Ew) /\
   (GF256_by_3 0xE4w = 0x37w) /\
   (GF256_by_3 0xE5w = 0x34w) /\
   (GF256_by_3 0xE6w = 0x31w) /\
   (GF256_by_3 0xE7w = 0x32w) /\
   (GF256_by_3 0xE8w = 0x23w) /\
   (GF256_by_3 0xE9w = 0x20w) /\
   (GF256_by_3 0xEAw = 0x25w) /\
   (GF256_by_3 0xEBw = 0x26w) /\
   (GF256_by_3 0xECw = 0x2Fw) /\
   (GF256_by_3 0xEDw = 0x2Cw) /\
   (GF256_by_3 0xEEw = 0x29w) /\
   (GF256_by_3 0xEFw = 0x2Aw) /\
   (GF256_by_3 0xF0w = 0xBw)  /\
   (GF256_by_3 0xF1w = 0x8w)  /\
   (GF256_by_3 0xF2w = 0xDw)  /\
   (GF256_by_3 0xF3w = 0xEw)  /\
   (GF256_by_3 0xF4w = 0x7w)  /\
   (GF256_by_3 0xF5w = 0x4w)  /\
   (GF256_by_3 0xF6w = 0x1w)  /\
   (GF256_by_3 0xF7w = 0x2w)  /\
   (GF256_by_3 0xF8w = 0x13w) /\
   (GF256_by_3 0xF9w = 0x10w) /\
   (GF256_by_3 0xFAw = 0x15w) /\
   (GF256_by_3 0xFBw = 0x16w) /\
   (GF256_by_3 0xFCw = 0x1Fw) /\
   (GF256_by_3 0xFDw = 0x1Cw) /\
   (GF256_by_3 0xFEw = 0x19w) /\
   (GF256_by_3 0xFFw = 0x1Aw)`;

val GF256_by_9 = Count.apply word8Define
  `(GF256_by_9 0x0w = 0x0w)  /\
   (GF256_by_9 0x1w = 0x9w)  /\
   (GF256_by_9 0x2w = 0x12w) /\
   (GF256_by_9 0x3w = 0x1Bw) /\
   (GF256_by_9 0x4w = 0x24w) /\
   (GF256_by_9 0x5w = 0x2Dw) /\
   (GF256_by_9 0x6w = 0x36w) /\
   (GF256_by_9 0x7w = 0x3Fw) /\
   (GF256_by_9 0x8w = 0x48w) /\
   (GF256_by_9 0x9w = 0x41w) /\
   (GF256_by_9 0xAw = 0x5Aw) /\
   (GF256_by_9 0xBw = 0x53w) /\
   (GF256_by_9 0xCw = 0x6Cw) /\
   (GF256_by_9 0xDw = 0x65w) /\
   (GF256_by_9 0xEw = 0x7Ew) /\
   (GF256_by_9 0xFw = 0x77w) /\
   (GF256_by_9 0x10w = 0x90w) /\
   (GF256_by_9 0x11w = 0x99w) /\
   (GF256_by_9 0x12w = 0x82w) /\
   (GF256_by_9 0x13w = 0x8Bw) /\
   (GF256_by_9 0x14w = 0xB4w) /\
   (GF256_by_9 0x15w = 0xBDw) /\
   (GF256_by_9 0x16w = 0xA6w) /\
   (GF256_by_9 0x17w = 0xAFw) /\
   (GF256_by_9 0x18w = 0xD8w) /\
   (GF256_by_9 0x19w = 0xD1w) /\
   (GF256_by_9 0x1Aw = 0xCAw) /\
   (GF256_by_9 0x1Bw = 0xC3w) /\
   (GF256_by_9 0x1Cw = 0xFCw) /\
   (GF256_by_9 0x1Dw = 0xF5w) /\
   (GF256_by_9 0x1Ew = 0xEEw) /\
   (GF256_by_9 0x1Fw = 0xE7w) /\
   (GF256_by_9 0x20w = 0x3Bw) /\
   (GF256_by_9 0x21w = 0x32w) /\
   (GF256_by_9 0x22w = 0x29w) /\
   (GF256_by_9 0x23w = 0x20w) /\
   (GF256_by_9 0x24w = 0x1Fw) /\
   (GF256_by_9 0x25w = 0x16w) /\
   (GF256_by_9 0x26w = 0xDw)  /\
   (GF256_by_9 0x27w = 0x4w)  /\
   (GF256_by_9 0x28w = 0x73w) /\
   (GF256_by_9 0x29w = 0x7Aw) /\
   (GF256_by_9 0x2Aw = 0x61w) /\
   (GF256_by_9 0x2Bw = 0x68w) /\
   (GF256_by_9 0x2Cw = 0x57w) /\
   (GF256_by_9 0x2Dw = 0x5Ew) /\
   (GF256_by_9 0x2Ew = 0x45w) /\
   (GF256_by_9 0x2Fw = 0x4Cw) /\
   (GF256_by_9 0x30w = 0xABw) /\
   (GF256_by_9 0x31w = 0xA2w) /\
   (GF256_by_9 0x32w = 0xB9w) /\
   (GF256_by_9 0x33w = 0xB0w) /\
   (GF256_by_9 0x34w = 0x8Fw) /\
   (GF256_by_9 0x35w = 0x86w) /\
   (GF256_by_9 0x36w = 0x9Dw) /\
   (GF256_by_9 0x37w = 0x94w) /\
   (GF256_by_9 0x38w = 0xE3w) /\
   (GF256_by_9 0x39w = 0xEAw) /\
   (GF256_by_9 0x3Aw = 0xF1w) /\
   (GF256_by_9 0x3Bw = 0xF8w) /\
   (GF256_by_9 0x3Cw = 0xC7w) /\
   (GF256_by_9 0x3Dw = 0xCEw) /\
   (GF256_by_9 0x3Ew = 0xD5w) /\
   (GF256_by_9 0x3Fw = 0xDCw) /\
   (GF256_by_9 0x40w = 0x76w) /\
   (GF256_by_9 0x41w = 0x7Fw) /\
   (GF256_by_9 0x42w = 0x64w) /\
   (GF256_by_9 0x43w = 0x6Dw) /\
   (GF256_by_9 0x44w = 0x52w) /\
   (GF256_by_9 0x45w = 0x5Bw) /\
   (GF256_by_9 0x46w = 0x40w) /\
   (GF256_by_9 0x47w = 0x49w) /\
   (GF256_by_9 0x48w = 0x3Ew) /\
   (GF256_by_9 0x49w = 0x37w) /\
   (GF256_by_9 0x4Aw = 0x2Cw) /\
   (GF256_by_9 0x4Bw = 0x25w) /\
   (GF256_by_9 0x4Cw = 0x1Aw) /\
   (GF256_by_9 0x4Dw = 0x13w) /\
   (GF256_by_9 0x4Ew = 0x8w)  /\
   (GF256_by_9 0x4Fw = 0x1w)  /\
   (GF256_by_9 0x50w = 0xE6w) /\
   (GF256_by_9 0x51w = 0xEFw) /\
   (GF256_by_9 0x52w = 0xF4w) /\
   (GF256_by_9 0x53w = 0xFDw) /\
   (GF256_by_9 0x54w = 0xC2w) /\
   (GF256_by_9 0x55w = 0xCBw) /\
   (GF256_by_9 0x56w = 0xD0w) /\
   (GF256_by_9 0x57w = 0xD9w) /\
   (GF256_by_9 0x58w = 0xAEw) /\
   (GF256_by_9 0x59w = 0xA7w) /\
   (GF256_by_9 0x5Aw = 0xBCw) /\
   (GF256_by_9 0x5Bw = 0xB5w) /\
   (GF256_by_9 0x5Cw = 0x8Aw) /\
   (GF256_by_9 0x5Dw = 0x83w) /\
   (GF256_by_9 0x5Ew = 0x98w) /\
   (GF256_by_9 0x5Fw = 0x91w) /\
   (GF256_by_9 0x60w = 0x4Dw) /\
   (GF256_by_9 0x61w = 0x44w) /\
   (GF256_by_9 0x62w = 0x5Fw) /\
   (GF256_by_9 0x63w = 0x56w) /\
   (GF256_by_9 0x64w = 0x69w) /\
   (GF256_by_9 0x65w = 0x60w) /\
   (GF256_by_9 0x66w = 0x7Bw) /\
   (GF256_by_9 0x67w = 0x72w) /\
   (GF256_by_9 0x68w = 0x5w)  /\
   (GF256_by_9 0x69w = 0xCw)  /\
   (GF256_by_9 0x6Aw = 0x17w) /\
   (GF256_by_9 0x6Bw = 0x1Ew) /\
   (GF256_by_9 0x6Cw = 0x21w) /\
   (GF256_by_9 0x6Dw = 0x28w) /\
   (GF256_by_9 0x6Ew = 0x33w) /\
   (GF256_by_9 0x6Fw = 0x3Aw) /\
   (GF256_by_9 0x70w = 0xDDw) /\
   (GF256_by_9 0x71w = 0xD4w) /\
   (GF256_by_9 0x72w = 0xCFw) /\
   (GF256_by_9 0x73w = 0xC6w) /\
   (GF256_by_9 0x74w = 0xF9w) /\
   (GF256_by_9 0x75w = 0xF0w) /\
   (GF256_by_9 0x76w = 0xEBw) /\
   (GF256_by_9 0x77w = 0xE2w) /\
   (GF256_by_9 0x78w = 0x95w) /\
   (GF256_by_9 0x79w = 0x9Cw) /\
   (GF256_by_9 0x7Aw = 0x87w) /\
   (GF256_by_9 0x7Bw = 0x8Ew) /\
   (GF256_by_9 0x7Cw = 0xB1w) /\
   (GF256_by_9 0x7Dw = 0xB8w) /\
   (GF256_by_9 0x7Ew = 0xA3w) /\
   (GF256_by_9 0x7Fw = 0xAAw) /\
   (GF256_by_9 0x80w = 0xECw) /\
   (GF256_by_9 0x81w = 0xE5w) /\
   (GF256_by_9 0x82w = 0xFEw) /\
   (GF256_by_9 0x83w = 0xF7w) /\
   (GF256_by_9 0x84w = 0xC8w) /\
   (GF256_by_9 0x85w = 0xC1w) /\
   (GF256_by_9 0x86w = 0xDAw) /\
   (GF256_by_9 0x87w = 0xD3w) /\
   (GF256_by_9 0x88w = 0xA4w) /\
   (GF256_by_9 0x89w = 0xADw) /\
   (GF256_by_9 0x8Aw = 0xB6w) /\
   (GF256_by_9 0x8Bw = 0xBFw) /\
   (GF256_by_9 0x8Cw = 0x80w) /\
   (GF256_by_9 0x8Dw = 0x89w) /\
   (GF256_by_9 0x8Ew = 0x92w) /\
   (GF256_by_9 0x8Fw = 0x9Bw) /\
   (GF256_by_9 0x90w = 0x7Cw) /\
   (GF256_by_9 0x91w = 0x75w) /\
   (GF256_by_9 0x92w = 0x6Ew) /\
   (GF256_by_9 0x93w = 0x67w) /\
   (GF256_by_9 0x94w = 0x58w) /\
   (GF256_by_9 0x95w = 0x51w) /\
   (GF256_by_9 0x96w = 0x4Aw) /\
   (GF256_by_9 0x97w = 0x43w) /\
   (GF256_by_9 0x98w = 0x34w) /\
   (GF256_by_9 0x99w = 0x3Dw) /\
   (GF256_by_9 0x9Aw = 0x26w) /\
   (GF256_by_9 0x9Bw = 0x2Fw) /\
   (GF256_by_9 0x9Cw = 0x10w) /\
   (GF256_by_9 0x9Dw = 0x19w) /\
   (GF256_by_9 0x9Ew = 0x2w)  /\
   (GF256_by_9 0x9Fw = 0xBw)  /\
   (GF256_by_9 0xA0w = 0xD7w) /\
   (GF256_by_9 0xA1w = 0xDEw) /\
   (GF256_by_9 0xA2w = 0xC5w) /\
   (GF256_by_9 0xA3w = 0xCCw) /\
   (GF256_by_9 0xA4w = 0xF3w) /\
   (GF256_by_9 0xA5w = 0xFAw) /\
   (GF256_by_9 0xA6w = 0xE1w) /\
   (GF256_by_9 0xA7w = 0xE8w) /\
   (GF256_by_9 0xA8w = 0x9Fw) /\
   (GF256_by_9 0xA9w = 0x96w) /\
   (GF256_by_9 0xAAw = 0x8Dw) /\
   (GF256_by_9 0xABw = 0x84w) /\
   (GF256_by_9 0xACw = 0xBBw) /\
   (GF256_by_9 0xADw = 0xB2w) /\
   (GF256_by_9 0xAEw = 0xA9w) /\
   (GF256_by_9 0xAFw = 0xA0w) /\
   (GF256_by_9 0xB0w = 0x47w) /\
   (GF256_by_9 0xB1w = 0x4Ew) /\
   (GF256_by_9 0xB2w = 0x55w) /\
   (GF256_by_9 0xB3w = 0x5Cw) /\
   (GF256_by_9 0xB4w = 0x63w) /\
   (GF256_by_9 0xB5w = 0x6Aw) /\
   (GF256_by_9 0xB6w = 0x71w) /\
   (GF256_by_9 0xB7w = 0x78w) /\
   (GF256_by_9 0xB8w = 0xFw)  /\
   (GF256_by_9 0xB9w = 0x6w)  /\
   (GF256_by_9 0xBAw = 0x1Dw) /\
   (GF256_by_9 0xBBw = 0x14w) /\
   (GF256_by_9 0xBCw = 0x2Bw) /\
   (GF256_by_9 0xBDw = 0x22w) /\
   (GF256_by_9 0xBEw = 0x39w) /\
   (GF256_by_9 0xBFw = 0x30w) /\
   (GF256_by_9 0xC0w = 0x9Aw) /\
   (GF256_by_9 0xC1w = 0x93w) /\
   (GF256_by_9 0xC2w = 0x88w) /\
   (GF256_by_9 0xC3w = 0x81w) /\
   (GF256_by_9 0xC4w = 0xBEw) /\
   (GF256_by_9 0xC5w = 0xB7w) /\
   (GF256_by_9 0xC6w = 0xACw) /\
   (GF256_by_9 0xC7w = 0xA5w) /\
   (GF256_by_9 0xC8w = 0xD2w) /\
   (GF256_by_9 0xC9w = 0xDBw) /\
   (GF256_by_9 0xCAw = 0xC0w) /\
   (GF256_by_9 0xCBw = 0xC9w) /\
   (GF256_by_9 0xCCw = 0xF6w) /\
   (GF256_by_9 0xCDw = 0xFFw) /\
   (GF256_by_9 0xCEw = 0xE4w) /\
   (GF256_by_9 0xCFw = 0xEDw) /\
   (GF256_by_9 0xD0w = 0xAw)  /\
   (GF256_by_9 0xD1w = 0x3w)  /\
   (GF256_by_9 0xD2w = 0x18w) /\
   (GF256_by_9 0xD3w = 0x11w) /\
   (GF256_by_9 0xD4w = 0x2Ew) /\
   (GF256_by_9 0xD5w = 0x27w) /\
   (GF256_by_9 0xD6w = 0x3Cw) /\
   (GF256_by_9 0xD7w = 0x35w) /\
   (GF256_by_9 0xD8w = 0x42w) /\
   (GF256_by_9 0xD9w = 0x4Bw) /\
   (GF256_by_9 0xDAw = 0x50w) /\
   (GF256_by_9 0xDBw = 0x59w) /\
   (GF256_by_9 0xDCw = 0x66w) /\
   (GF256_by_9 0xDDw = 0x6Fw) /\
   (GF256_by_9 0xDEw = 0x74w) /\
   (GF256_by_9 0xDFw = 0x7Dw) /\
   (GF256_by_9 0xE0w = 0xA1w) /\
   (GF256_by_9 0xE1w = 0xA8w) /\
   (GF256_by_9 0xE2w = 0xB3w) /\
   (GF256_by_9 0xE3w = 0xBAw) /\
   (GF256_by_9 0xE4w = 0x85w) /\
   (GF256_by_9 0xE5w = 0x8Cw) /\
   (GF256_by_9 0xE6w = 0x97w) /\
   (GF256_by_9 0xE7w = 0x9Ew) /\
   (GF256_by_9 0xE8w = 0xE9w) /\
   (GF256_by_9 0xE9w = 0xE0w) /\
   (GF256_by_9 0xEAw = 0xFBw) /\
   (GF256_by_9 0xEBw = 0xF2w) /\
   (GF256_by_9 0xECw = 0xCDw) /\
   (GF256_by_9 0xEDw = 0xC4w) /\
   (GF256_by_9 0xEEw = 0xDFw) /\
   (GF256_by_9 0xEFw = 0xD6w) /\
   (GF256_by_9 0xF0w = 0x31w) /\
   (GF256_by_9 0xF1w = 0x38w) /\
   (GF256_by_9 0xF2w = 0x23w) /\
   (GF256_by_9 0xF3w = 0x2Aw) /\
   (GF256_by_9 0xF4w = 0x15w) /\
   (GF256_by_9 0xF5w = 0x1Cw) /\
   (GF256_by_9 0xF6w = 0x7w)  /\
   (GF256_by_9 0xF7w = 0xEw)  /\
   (GF256_by_9 0xF8w = 0x79w) /\
   (GF256_by_9 0xF9w = 0x70w) /\
   (GF256_by_9 0xFAw = 0x6Bw) /\
   (GF256_by_9 0xFBw = 0x62w) /\
   (GF256_by_9 0xFCw = 0x5Dw) /\
   (GF256_by_9 0xFDw = 0x54w) /\
   (GF256_by_9 0xFEw = 0x4Fw) /\
   (GF256_by_9 0xFFw = 0x46w)`;

val GF256_by_11 = Count.apply word8Define
  `(GF256_by_11 0x0w = 0x0w)  /\
   (GF256_by_11 0x1w = 0xBw)  /\
   (GF256_by_11 0x2w = 0x16w) /\
   (GF256_by_11 0x3w = 0x1Dw) /\
   (GF256_by_11 0x4w = 0x2Cw) /\
   (GF256_by_11 0x5w = 0x27w) /\
   (GF256_by_11 0x6w = 0x3Aw) /\
   (GF256_by_11 0x7w = 0x31w) /\
   (GF256_by_11 0x8w = 0x58w) /\
   (GF256_by_11 0x9w = 0x53w) /\
   (GF256_by_11 0xAw = 0x4Ew) /\
   (GF256_by_11 0xBw = 0x45w) /\
   (GF256_by_11 0xCw = 0x74w) /\
   (GF256_by_11 0xDw = 0x7Fw) /\
   (GF256_by_11 0xEw = 0x62w) /\
   (GF256_by_11 0xFw = 0x69w) /\
   (GF256_by_11 0x10w = 0xB0w) /\
   (GF256_by_11 0x11w = 0xBBw) /\
   (GF256_by_11 0x12w = 0xA6w) /\
   (GF256_by_11 0x13w = 0xADw) /\
   (GF256_by_11 0x14w = 0x9Cw) /\
   (GF256_by_11 0x15w = 0x97w) /\
   (GF256_by_11 0x16w = 0x8Aw) /\
   (GF256_by_11 0x17w = 0x81w) /\
   (GF256_by_11 0x18w = 0xE8w) /\
   (GF256_by_11 0x19w = 0xE3w) /\
   (GF256_by_11 0x1Aw = 0xFEw) /\
   (GF256_by_11 0x1Bw = 0xF5w) /\
   (GF256_by_11 0x1Cw = 0xC4w) /\
   (GF256_by_11 0x1Dw = 0xCFw) /\
   (GF256_by_11 0x1Ew = 0xD2w) /\
   (GF256_by_11 0x1Fw = 0xD9w) /\
   (GF256_by_11 0x20w = 0x7Bw) /\
   (GF256_by_11 0x21w = 0x70w) /\
   (GF256_by_11 0x22w = 0x6Dw) /\
   (GF256_by_11 0x23w = 0x66w) /\
   (GF256_by_11 0x24w = 0x57w) /\
   (GF256_by_11 0x25w = 0x5Cw) /\
   (GF256_by_11 0x26w = 0x41w) /\
   (GF256_by_11 0x27w = 0x4Aw) /\
   (GF256_by_11 0x28w = 0x23w) /\
   (GF256_by_11 0x29w = 0x28w) /\
   (GF256_by_11 0x2Aw = 0x35w) /\
   (GF256_by_11 0x2Bw = 0x3Ew) /\
   (GF256_by_11 0x2Cw = 0xFw)  /\
   (GF256_by_11 0x2Dw = 0x4w)  /\
   (GF256_by_11 0x2Ew = 0x19w) /\
   (GF256_by_11 0x2Fw = 0x12w) /\
   (GF256_by_11 0x30w = 0xCBw) /\
   (GF256_by_11 0x31w = 0xC0w) /\
   (GF256_by_11 0x32w = 0xDDw) /\
   (GF256_by_11 0x33w = 0xD6w) /\
   (GF256_by_11 0x34w = 0xE7w) /\
   (GF256_by_11 0x35w = 0xECw) /\
   (GF256_by_11 0x36w = 0xF1w) /\
   (GF256_by_11 0x37w = 0xFAw) /\
   (GF256_by_11 0x38w = 0x93w) /\
   (GF256_by_11 0x39w = 0x98w) /\
   (GF256_by_11 0x3Aw = 0x85w) /\
   (GF256_by_11 0x3Bw = 0x8Ew) /\
   (GF256_by_11 0x3Cw = 0xBFw) /\
   (GF256_by_11 0x3Dw = 0xB4w) /\
   (GF256_by_11 0x3Ew = 0xA9w) /\
   (GF256_by_11 0x3Fw = 0xA2w) /\
   (GF256_by_11 0x40w = 0xF6w) /\
   (GF256_by_11 0x41w = 0xFDw) /\
   (GF256_by_11 0x42w = 0xE0w) /\
   (GF256_by_11 0x43w = 0xEBw) /\
   (GF256_by_11 0x44w = 0xDAw) /\
   (GF256_by_11 0x45w = 0xD1w) /\
   (GF256_by_11 0x46w = 0xCCw) /\
   (GF256_by_11 0x47w = 0xC7w) /\
   (GF256_by_11 0x48w = 0xAEw) /\
   (GF256_by_11 0x49w = 0xA5w) /\
   (GF256_by_11 0x4Aw = 0xB8w) /\
   (GF256_by_11 0x4Bw = 0xB3w) /\
   (GF256_by_11 0x4Cw = 0x82w) /\
   (GF256_by_11 0x4Dw = 0x89w) /\
   (GF256_by_11 0x4Ew = 0x94w) /\
   (GF256_by_11 0x4Fw = 0x9Fw) /\
   (GF256_by_11 0x50w = 0x46w) /\
   (GF256_by_11 0x51w = 0x4Dw) /\
   (GF256_by_11 0x52w = 0x50w) /\
   (GF256_by_11 0x53w = 0x5Bw) /\
   (GF256_by_11 0x54w = 0x6Aw) /\
   (GF256_by_11 0x55w = 0x61w) /\
   (GF256_by_11 0x56w = 0x7Cw) /\
   (GF256_by_11 0x57w = 0x77w) /\
   (GF256_by_11 0x58w = 0x1Ew) /\
   (GF256_by_11 0x59w = 0x15w) /\
   (GF256_by_11 0x5Aw = 0x8w)  /\
   (GF256_by_11 0x5Bw = 0x3w)  /\
   (GF256_by_11 0x5Cw = 0x32w) /\
   (GF256_by_11 0x5Dw = 0x39w) /\
   (GF256_by_11 0x5Ew = 0x24w) /\
   (GF256_by_11 0x5Fw = 0x2Fw) /\
   (GF256_by_11 0x60w = 0x8Dw) /\
   (GF256_by_11 0x61w = 0x86w) /\
   (GF256_by_11 0x62w = 0x9Bw) /\
   (GF256_by_11 0x63w = 0x90w) /\
   (GF256_by_11 0x64w = 0xA1w) /\
   (GF256_by_11 0x65w = 0xAAw) /\
   (GF256_by_11 0x66w = 0xB7w) /\
   (GF256_by_11 0x67w = 0xBCw) /\
   (GF256_by_11 0x68w = 0xD5w) /\
   (GF256_by_11 0x69w = 0xDEw) /\
   (GF256_by_11 0x6Aw = 0xC3w) /\
   (GF256_by_11 0x6Bw = 0xC8w) /\
   (GF256_by_11 0x6Cw = 0xF9w) /\
   (GF256_by_11 0x6Dw = 0xF2w) /\
   (GF256_by_11 0x6Ew = 0xEFw) /\
   (GF256_by_11 0x6Fw = 0xE4w) /\
   (GF256_by_11 0x70w = 0x3Dw) /\
   (GF256_by_11 0x71w = 0x36w) /\
   (GF256_by_11 0x72w = 0x2Bw) /\
   (GF256_by_11 0x73w = 0x20w) /\
   (GF256_by_11 0x74w = 0x11w) /\
   (GF256_by_11 0x75w = 0x1Aw) /\
   (GF256_by_11 0x76w = 0x7w)  /\
   (GF256_by_11 0x77w = 0xCw)  /\
   (GF256_by_11 0x78w = 0x65w) /\
   (GF256_by_11 0x79w = 0x6Ew) /\
   (GF256_by_11 0x7Aw = 0x73w) /\
   (GF256_by_11 0x7Bw = 0x78w) /\
   (GF256_by_11 0x7Cw = 0x49w) /\
   (GF256_by_11 0x7Dw = 0x42w) /\
   (GF256_by_11 0x7Ew = 0x5Fw) /\
   (GF256_by_11 0x7Fw = 0x54w) /\
   (GF256_by_11 0x80w = 0xF7w) /\
   (GF256_by_11 0x81w = 0xFCw) /\
   (GF256_by_11 0x82w = 0xE1w) /\
   (GF256_by_11 0x83w = 0xEAw) /\
   (GF256_by_11 0x84w = 0xDBw) /\
   (GF256_by_11 0x85w = 0xD0w) /\
   (GF256_by_11 0x86w = 0xCDw) /\
   (GF256_by_11 0x87w = 0xC6w) /\
   (GF256_by_11 0x88w = 0xAFw) /\
   (GF256_by_11 0x89w = 0xA4w) /\
   (GF256_by_11 0x8Aw = 0xB9w) /\
   (GF256_by_11 0x8Bw = 0xB2w) /\
   (GF256_by_11 0x8Cw = 0x83w) /\
   (GF256_by_11 0x8Dw = 0x88w) /\
   (GF256_by_11 0x8Ew = 0x95w) /\
   (GF256_by_11 0x8Fw = 0x9Ew) /\
   (GF256_by_11 0x90w = 0x47w) /\
   (GF256_by_11 0x91w = 0x4Cw) /\
   (GF256_by_11 0x92w = 0x51w) /\
   (GF256_by_11 0x93w = 0x5Aw) /\
   (GF256_by_11 0x94w = 0x6Bw) /\
   (GF256_by_11 0x95w = 0x60w) /\
   (GF256_by_11 0x96w = 0x7Dw) /\
   (GF256_by_11 0x97w = 0x76w) /\
   (GF256_by_11 0x98w = 0x1Fw) /\
   (GF256_by_11 0x99w = 0x14w) /\
   (GF256_by_11 0x9Aw = 0x9w)  /\
   (GF256_by_11 0x9Bw = 0x2w)  /\
   (GF256_by_11 0x9Cw = 0x33w) /\
   (GF256_by_11 0x9Dw = 0x38w) /\
   (GF256_by_11 0x9Ew = 0x25w) /\
   (GF256_by_11 0x9Fw = 0x2Ew) /\
   (GF256_by_11 0xA0w = 0x8Cw) /\
   (GF256_by_11 0xA1w = 0x87w) /\
   (GF256_by_11 0xA2w = 0x9Aw) /\
   (GF256_by_11 0xA3w = 0x91w) /\
   (GF256_by_11 0xA4w = 0xA0w) /\
   (GF256_by_11 0xA5w = 0xABw) /\
   (GF256_by_11 0xA6w = 0xB6w) /\
   (GF256_by_11 0xA7w = 0xBDw) /\
   (GF256_by_11 0xA8w = 0xD4w) /\
   (GF256_by_11 0xA9w = 0xDFw) /\
   (GF256_by_11 0xAAw = 0xC2w) /\
   (GF256_by_11 0xABw = 0xC9w) /\
   (GF256_by_11 0xACw = 0xF8w) /\
   (GF256_by_11 0xADw = 0xF3w) /\
   (GF256_by_11 0xAEw = 0xEEw) /\
   (GF256_by_11 0xAFw = 0xE5w) /\
   (GF256_by_11 0xB0w = 0x3Cw) /\
   (GF256_by_11 0xB1w = 0x37w) /\
   (GF256_by_11 0xB2w = 0x2Aw) /\
   (GF256_by_11 0xB3w = 0x21w) /\
   (GF256_by_11 0xB4w = 0x10w) /\
   (GF256_by_11 0xB5w = 0x1Bw) /\
   (GF256_by_11 0xB6w = 0x6w)  /\
   (GF256_by_11 0xB7w = 0xDw)  /\
   (GF256_by_11 0xB8w = 0x64w) /\
   (GF256_by_11 0xB9w = 0x6Fw) /\
   (GF256_by_11 0xBAw = 0x72w) /\
   (GF256_by_11 0xBBw = 0x79w) /\
   (GF256_by_11 0xBCw = 0x48w) /\
   (GF256_by_11 0xBDw = 0x43w) /\
   (GF256_by_11 0xBEw = 0x5Ew) /\
   (GF256_by_11 0xBFw = 0x55w) /\
   (GF256_by_11 0xC0w = 0x1w)  /\
   (GF256_by_11 0xC1w = 0xAw)  /\
   (GF256_by_11 0xC2w = 0x17w) /\
   (GF256_by_11 0xC3w = 0x1Cw) /\
   (GF256_by_11 0xC4w = 0x2Dw) /\
   (GF256_by_11 0xC5w = 0x26w) /\
   (GF256_by_11 0xC6w = 0x3Bw) /\
   (GF256_by_11 0xC7w = 0x30w) /\
   (GF256_by_11 0xC8w = 0x59w) /\
   (GF256_by_11 0xC9w = 0x52w) /\
   (GF256_by_11 0xCAw = 0x4Fw) /\
   (GF256_by_11 0xCBw = 0x44w) /\
   (GF256_by_11 0xCCw = 0x75w) /\
   (GF256_by_11 0xCDw = 0x7Ew) /\
   (GF256_by_11 0xCEw = 0x63w) /\
   (GF256_by_11 0xCFw = 0x68w) /\
   (GF256_by_11 0xD0w = 0xB1w) /\
   (GF256_by_11 0xD1w = 0xBAw) /\
   (GF256_by_11 0xD2w = 0xA7w) /\
   (GF256_by_11 0xD3w = 0xACw) /\
   (GF256_by_11 0xD4w = 0x9Dw) /\
   (GF256_by_11 0xD5w = 0x96w) /\
   (GF256_by_11 0xD6w = 0x8Bw) /\
   (GF256_by_11 0xD7w = 0x80w) /\
   (GF256_by_11 0xD8w = 0xE9w) /\
   (GF256_by_11 0xD9w = 0xE2w) /\
   (GF256_by_11 0xDAw = 0xFFw) /\
   (GF256_by_11 0xDBw = 0xF4w) /\
   (GF256_by_11 0xDCw = 0xC5w) /\
   (GF256_by_11 0xDDw = 0xCEw) /\
   (GF256_by_11 0xDEw = 0xD3w) /\
   (GF256_by_11 0xDFw = 0xD8w) /\
   (GF256_by_11 0xE0w = 0x7Aw) /\
   (GF256_by_11 0xE1w = 0x71w) /\
   (GF256_by_11 0xE2w = 0x6Cw) /\
   (GF256_by_11 0xE3w = 0x67w) /\
   (GF256_by_11 0xE4w = 0x56w) /\
   (GF256_by_11 0xE5w = 0x5Dw) /\
   (GF256_by_11 0xE6w = 0x40w) /\
   (GF256_by_11 0xE7w = 0x4Bw) /\
   (GF256_by_11 0xE8w = 0x22w) /\
   (GF256_by_11 0xE9w = 0x29w) /\
   (GF256_by_11 0xEAw = 0x34w) /\
   (GF256_by_11 0xEBw = 0x3Fw) /\
   (GF256_by_11 0xECw = 0xEw)  /\
   (GF256_by_11 0xEDw = 0x5w)  /\
   (GF256_by_11 0xEEw = 0x18w) /\
   (GF256_by_11 0xEFw = 0x13w) /\
   (GF256_by_11 0xF0w = 0xCAw) /\
   (GF256_by_11 0xF1w = 0xC1w) /\
   (GF256_by_11 0xF2w = 0xDCw) /\
   (GF256_by_11 0xF3w = 0xD7w) /\
   (GF256_by_11 0xF4w = 0xE6w) /\
   (GF256_by_11 0xF5w = 0xEDw) /\
   (GF256_by_11 0xF6w = 0xF0w) /\
   (GF256_by_11 0xF7w = 0xFBw) /\
   (GF256_by_11 0xF8w = 0x92w) /\
   (GF256_by_11 0xF9w = 0x99w) /\
   (GF256_by_11 0xFAw = 0x84w) /\
   (GF256_by_11 0xFBw = 0x8Fw) /\
   (GF256_by_11 0xFCw = 0xBEw) /\
   (GF256_by_11 0xFDw = 0xB5w) /\
   (GF256_by_11 0xFEw = 0xA8w) /\
   (GF256_by_11 0xFFw = 0xA3w)`;

val GF256_by_13 = Count.apply word8Define
  `(GF256_by_13 0x0w = 0x0w)  /\
   (GF256_by_13 0x1w = 0xDw)  /\
   (GF256_by_13 0x2w = 0x1Aw) /\
   (GF256_by_13 0x3w = 0x17w) /\
   (GF256_by_13 0x4w = 0x34w) /\
   (GF256_by_13 0x5w = 0x39w) /\
   (GF256_by_13 0x6w = 0x2Ew) /\
   (GF256_by_13 0x7w = 0x23w) /\
   (GF256_by_13 0x8w = 0x68w) /\
   (GF256_by_13 0x9w = 0x65w) /\
   (GF256_by_13 0xAw = 0x72w) /\
   (GF256_by_13 0xBw = 0x7Fw) /\
   (GF256_by_13 0xCw = 0x5Cw) /\
   (GF256_by_13 0xDw = 0x51w) /\
   (GF256_by_13 0xEw = 0x46w) /\
   (GF256_by_13 0xFw = 0x4Bw) /\
   (GF256_by_13 0x10w = 0xD0w) /\
   (GF256_by_13 0x11w = 0xDDw) /\
   (GF256_by_13 0x12w = 0xCAw) /\
   (GF256_by_13 0x13w = 0xC7w) /\
   (GF256_by_13 0x14w = 0xE4w) /\
   (GF256_by_13 0x15w = 0xE9w) /\
   (GF256_by_13 0x16w = 0xFEw) /\
   (GF256_by_13 0x17w = 0xF3w) /\
   (GF256_by_13 0x18w = 0xB8w) /\
   (GF256_by_13 0x19w = 0xB5w) /\
   (GF256_by_13 0x1Aw = 0xA2w) /\
   (GF256_by_13 0x1Bw = 0xAFw) /\
   (GF256_by_13 0x1Cw = 0x8Cw) /\
   (GF256_by_13 0x1Dw = 0x81w) /\
   (GF256_by_13 0x1Ew = 0x96w) /\
   (GF256_by_13 0x1Fw = 0x9Bw) /\
   (GF256_by_13 0x20w = 0xBBw) /\
   (GF256_by_13 0x21w = 0xB6w) /\
   (GF256_by_13 0x22w = 0xA1w) /\
   (GF256_by_13 0x23w = 0xACw) /\
   (GF256_by_13 0x24w = 0x8Fw) /\
   (GF256_by_13 0x25w = 0x82w) /\
   (GF256_by_13 0x26w = 0x95w) /\
   (GF256_by_13 0x27w = 0x98w) /\
   (GF256_by_13 0x28w = 0xD3w) /\
   (GF256_by_13 0x29w = 0xDEw) /\
   (GF256_by_13 0x2Aw = 0xC9w) /\
   (GF256_by_13 0x2Bw = 0xC4w) /\
   (GF256_by_13 0x2Cw = 0xE7w) /\
   (GF256_by_13 0x2Dw = 0xEAw) /\
   (GF256_by_13 0x2Ew = 0xFDw) /\
   (GF256_by_13 0x2Fw = 0xF0w) /\
   (GF256_by_13 0x30w = 0x6Bw) /\
   (GF256_by_13 0x31w = 0x66w) /\
   (GF256_by_13 0x32w = 0x71w) /\
   (GF256_by_13 0x33w = 0x7Cw) /\
   (GF256_by_13 0x34w = 0x5Fw) /\
   (GF256_by_13 0x35w = 0x52w) /\
   (GF256_by_13 0x36w = 0x45w) /\
   (GF256_by_13 0x37w = 0x48w) /\
   (GF256_by_13 0x38w = 0x3w)  /\
   (GF256_by_13 0x39w = 0xEw)  /\
   (GF256_by_13 0x3Aw = 0x19w) /\
   (GF256_by_13 0x3Bw = 0x14w) /\
   (GF256_by_13 0x3Cw = 0x37w) /\
   (GF256_by_13 0x3Dw = 0x3Aw) /\
   (GF256_by_13 0x3Ew = 0x2Dw) /\
   (GF256_by_13 0x3Fw = 0x20w) /\
   (GF256_by_13 0x40w = 0x6Dw) /\
   (GF256_by_13 0x41w = 0x60w) /\
   (GF256_by_13 0x42w = 0x77w) /\
   (GF256_by_13 0x43w = 0x7Aw) /\
   (GF256_by_13 0x44w = 0x59w) /\
   (GF256_by_13 0x45w = 0x54w) /\
   (GF256_by_13 0x46w = 0x43w) /\
   (GF256_by_13 0x47w = 0x4Ew) /\
   (GF256_by_13 0x48w = 0x5w)  /\
   (GF256_by_13 0x49w = 0x8w)  /\
   (GF256_by_13 0x4Aw = 0x1Fw) /\
   (GF256_by_13 0x4Bw = 0x12w) /\
   (GF256_by_13 0x4Cw = 0x31w) /\
   (GF256_by_13 0x4Dw = 0x3Cw) /\
   (GF256_by_13 0x4Ew = 0x2Bw) /\
   (GF256_by_13 0x4Fw = 0x26w) /\
   (GF256_by_13 0x50w = 0xBDw) /\
   (GF256_by_13 0x51w = 0xB0w) /\
   (GF256_by_13 0x52w = 0xA7w) /\
   (GF256_by_13 0x53w = 0xAAw) /\
   (GF256_by_13 0x54w = 0x89w) /\
   (GF256_by_13 0x55w = 0x84w) /\
   (GF256_by_13 0x56w = 0x93w) /\
   (GF256_by_13 0x57w = 0x9Ew) /\
   (GF256_by_13 0x58w = 0xD5w) /\
   (GF256_by_13 0x59w = 0xD8w) /\
   (GF256_by_13 0x5Aw = 0xCFw) /\
   (GF256_by_13 0x5Bw = 0xC2w) /\
   (GF256_by_13 0x5Cw = 0xE1w) /\
   (GF256_by_13 0x5Dw = 0xECw) /\
   (GF256_by_13 0x5Ew = 0xFBw) /\
   (GF256_by_13 0x5Fw = 0xF6w) /\
   (GF256_by_13 0x60w = 0xD6w) /\
   (GF256_by_13 0x61w = 0xDBw) /\
   (GF256_by_13 0x62w = 0xCCw) /\
   (GF256_by_13 0x63w = 0xC1w) /\
   (GF256_by_13 0x64w = 0xE2w) /\
   (GF256_by_13 0x65w = 0xEFw) /\
   (GF256_by_13 0x66w = 0xF8w) /\
   (GF256_by_13 0x67w = 0xF5w) /\
   (GF256_by_13 0x68w = 0xBEw) /\
   (GF256_by_13 0x69w = 0xB3w) /\
   (GF256_by_13 0x6Aw = 0xA4w) /\
   (GF256_by_13 0x6Bw = 0xA9w) /\
   (GF256_by_13 0x6Cw = 0x8Aw) /\
   (GF256_by_13 0x6Dw = 0x87w) /\
   (GF256_by_13 0x6Ew = 0x90w) /\
   (GF256_by_13 0x6Fw = 0x9Dw) /\
   (GF256_by_13 0x70w = 0x6w)  /\
   (GF256_by_13 0x71w = 0xBw)  /\
   (GF256_by_13 0x72w = 0x1Cw) /\
   (GF256_by_13 0x73w = 0x11w) /\
   (GF256_by_13 0x74w = 0x32w) /\
   (GF256_by_13 0x75w = 0x3Fw) /\
   (GF256_by_13 0x76w = 0x28w) /\
   (GF256_by_13 0x77w = 0x25w) /\
   (GF256_by_13 0x78w = 0x6Ew) /\
   (GF256_by_13 0x79w = 0x63w) /\
   (GF256_by_13 0x7Aw = 0x74w) /\
   (GF256_by_13 0x7Bw = 0x79w) /\
   (GF256_by_13 0x7Cw = 0x5Aw) /\
   (GF256_by_13 0x7Dw = 0x57w) /\
   (GF256_by_13 0x7Ew = 0x40w) /\
   (GF256_by_13 0x7Fw = 0x4Dw) /\
   (GF256_by_13 0x80w = 0xDAw) /\
   (GF256_by_13 0x81w = 0xD7w) /\
   (GF256_by_13 0x82w = 0xC0w) /\
   (GF256_by_13 0x83w = 0xCDw) /\
   (GF256_by_13 0x84w = 0xEEw) /\
   (GF256_by_13 0x85w = 0xE3w) /\
   (GF256_by_13 0x86w = 0xF4w) /\
   (GF256_by_13 0x87w = 0xF9w) /\
   (GF256_by_13 0x88w = 0xB2w) /\
   (GF256_by_13 0x89w = 0xBFw) /\
   (GF256_by_13 0x8Aw = 0xA8w) /\
   (GF256_by_13 0x8Bw = 0xA5w) /\
   (GF256_by_13 0x8Cw = 0x86w) /\
   (GF256_by_13 0x8Dw = 0x8Bw) /\
   (GF256_by_13 0x8Ew = 0x9Cw) /\
   (GF256_by_13 0x8Fw = 0x91w) /\
   (GF256_by_13 0x90w = 0xAw)  /\
   (GF256_by_13 0x91w = 0x7w)  /\
   (GF256_by_13 0x92w = 0x10w) /\
   (GF256_by_13 0x93w = 0x1Dw) /\
   (GF256_by_13 0x94w = 0x3Ew) /\
   (GF256_by_13 0x95w = 0x33w) /\
   (GF256_by_13 0x96w = 0x24w) /\
   (GF256_by_13 0x97w = 0x29w) /\
   (GF256_by_13 0x98w = 0x62w) /\
   (GF256_by_13 0x99w = 0x6Fw) /\
   (GF256_by_13 0x9Aw = 0x78w) /\
   (GF256_by_13 0x9Bw = 0x75w) /\
   (GF256_by_13 0x9Cw = 0x56w) /\
   (GF256_by_13 0x9Dw = 0x5Bw) /\
   (GF256_by_13 0x9Ew = 0x4Cw) /\
   (GF256_by_13 0x9Fw = 0x41w) /\
   (GF256_by_13 0xA0w = 0x61w) /\
   (GF256_by_13 0xA1w = 0x6Cw) /\
   (GF256_by_13 0xA2w = 0x7Bw) /\
   (GF256_by_13 0xA3w = 0x76w) /\
   (GF256_by_13 0xA4w = 0x55w) /\
   (GF256_by_13 0xA5w = 0x58w) /\
   (GF256_by_13 0xA6w = 0x4Fw) /\
   (GF256_by_13 0xA7w = 0x42w) /\
   (GF256_by_13 0xA8w = 0x9w)  /\
   (GF256_by_13 0xA9w = 0x4w)  /\
   (GF256_by_13 0xAAw = 0x13w) /\
   (GF256_by_13 0xABw = 0x1Ew) /\
   (GF256_by_13 0xACw = 0x3Dw) /\
   (GF256_by_13 0xADw = 0x30w) /\
   (GF256_by_13 0xAEw = 0x27w) /\
   (GF256_by_13 0xAFw = 0x2Aw) /\
   (GF256_by_13 0xB0w = 0xB1w) /\
   (GF256_by_13 0xB1w = 0xBCw) /\
   (GF256_by_13 0xB2w = 0xABw) /\
   (GF256_by_13 0xB3w = 0xA6w) /\
   (GF256_by_13 0xB4w = 0x85w) /\
   (GF256_by_13 0xB5w = 0x88w) /\
   (GF256_by_13 0xB6w = 0x9Fw) /\
   (GF256_by_13 0xB7w = 0x92w) /\
   (GF256_by_13 0xB8w = 0xD9w) /\
   (GF256_by_13 0xB9w = 0xD4w) /\
   (GF256_by_13 0xBAw = 0xC3w) /\
   (GF256_by_13 0xBBw = 0xCEw) /\
   (GF256_by_13 0xBCw = 0xEDw) /\
   (GF256_by_13 0xBDw = 0xE0w) /\
   (GF256_by_13 0xBEw = 0xF7w) /\
   (GF256_by_13 0xBFw = 0xFAw) /\
   (GF256_by_13 0xC0w = 0xB7w) /\
   (GF256_by_13 0xC1w = 0xBAw) /\
   (GF256_by_13 0xC2w = 0xADw) /\
   (GF256_by_13 0xC3w = 0xA0w) /\
   (GF256_by_13 0xC4w = 0x83w) /\
   (GF256_by_13 0xC5w = 0x8Ew) /\
   (GF256_by_13 0xC6w = 0x99w) /\
   (GF256_by_13 0xC7w = 0x94w) /\
   (GF256_by_13 0xC8w = 0xDFw) /\
   (GF256_by_13 0xC9w = 0xD2w) /\
   (GF256_by_13 0xCAw = 0xC5w) /\
   (GF256_by_13 0xCBw = 0xC8w) /\
   (GF256_by_13 0xCCw = 0xEBw) /\
   (GF256_by_13 0xCDw = 0xE6w) /\
   (GF256_by_13 0xCEw = 0xF1w) /\
   (GF256_by_13 0xCFw = 0xFCw) /\
   (GF256_by_13 0xD0w = 0x67w) /\
   (GF256_by_13 0xD1w = 0x6Aw) /\
   (GF256_by_13 0xD2w = 0x7Dw) /\
   (GF256_by_13 0xD3w = 0x70w) /\
   (GF256_by_13 0xD4w = 0x53w) /\
   (GF256_by_13 0xD5w = 0x5Ew) /\
   (GF256_by_13 0xD6w = 0x49w) /\
   (GF256_by_13 0xD7w = 0x44w) /\
   (GF256_by_13 0xD8w = 0xFw)  /\
   (GF256_by_13 0xD9w = 0x2w)  /\
   (GF256_by_13 0xDAw = 0x15w) /\
   (GF256_by_13 0xDBw = 0x18w) /\
   (GF256_by_13 0xDCw = 0x3Bw) /\
   (GF256_by_13 0xDDw = 0x36w) /\
   (GF256_by_13 0xDEw = 0x21w) /\
   (GF256_by_13 0xDFw = 0x2Cw) /\
   (GF256_by_13 0xE0w = 0xCw)  /\
   (GF256_by_13 0xE1w = 0x1w)  /\
   (GF256_by_13 0xE2w = 0x16w) /\
   (GF256_by_13 0xE3w = 0x1Bw) /\
   (GF256_by_13 0xE4w = 0x38w) /\
   (GF256_by_13 0xE5w = 0x35w) /\
   (GF256_by_13 0xE6w = 0x22w) /\
   (GF256_by_13 0xE7w = 0x2Fw) /\
   (GF256_by_13 0xE8w = 0x64w) /\
   (GF256_by_13 0xE9w = 0x69w) /\
   (GF256_by_13 0xEAw = 0x7Ew) /\
   (GF256_by_13 0xEBw = 0x73w) /\
   (GF256_by_13 0xECw = 0x50w) /\
   (GF256_by_13 0xEDw = 0x5Dw) /\
   (GF256_by_13 0xEEw = 0x4Aw) /\
   (GF256_by_13 0xEFw = 0x47w) /\
   (GF256_by_13 0xF0w = 0xDCw) /\
   (GF256_by_13 0xF1w = 0xD1w) /\
   (GF256_by_13 0xF2w = 0xC6w) /\
   (GF256_by_13 0xF3w = 0xCBw) /\
   (GF256_by_13 0xF4w = 0xE8w) /\
   (GF256_by_13 0xF5w = 0xE5w) /\
   (GF256_by_13 0xF6w = 0xF2w) /\
   (GF256_by_13 0xF7w = 0xFFw) /\
   (GF256_by_13 0xF8w = 0xB4w) /\
   (GF256_by_13 0xF9w = 0xB9w) /\
   (GF256_by_13 0xFAw = 0xAEw) /\
   (GF256_by_13 0xFBw = 0xA3w) /\
   (GF256_by_13 0xFCw = 0x80w) /\
   (GF256_by_13 0xFDw = 0x8Dw) /\
   (GF256_by_13 0xFEw = 0x9Aw) /\
   (GF256_by_13 0xFFw = 0x97w)`;

val GF256_by_14 = Count.apply word8Define
  `(GF256_by_14 0x0w = 0x0w)  /\
   (GF256_by_14 0x1w = 0xEw)  /\
   (GF256_by_14 0x2w = 0x1Cw) /\
   (GF256_by_14 0x3w = 0x12w) /\
   (GF256_by_14 0x4w = 0x38w) /\
   (GF256_by_14 0x5w = 0x36w) /\
   (GF256_by_14 0x6w = 0x24w) /\
   (GF256_by_14 0x7w = 0x2Aw) /\
   (GF256_by_14 0x8w = 0x70w) /\
   (GF256_by_14 0x9w = 0x7Ew) /\
   (GF256_by_14 0xAw = 0x6Cw) /\
   (GF256_by_14 0xBw = 0x62w) /\
   (GF256_by_14 0xCw = 0x48w) /\
   (GF256_by_14 0xDw = 0x46w) /\
   (GF256_by_14 0xEw = 0x54w) /\
   (GF256_by_14 0xFw = 0x5Aw) /\
   (GF256_by_14 0x10w = 0xE0w) /\
   (GF256_by_14 0x11w = 0xEEw) /\
   (GF256_by_14 0x12w = 0xFCw) /\
   (GF256_by_14 0x13w = 0xF2w) /\
   (GF256_by_14 0x14w = 0xD8w) /\
   (GF256_by_14 0x15w = 0xD6w) /\
   (GF256_by_14 0x16w = 0xC4w) /\
   (GF256_by_14 0x17w = 0xCAw) /\
   (GF256_by_14 0x18w = 0x90w) /\
   (GF256_by_14 0x19w = 0x9Ew) /\
   (GF256_by_14 0x1Aw = 0x8Cw) /\
   (GF256_by_14 0x1Bw = 0x82w) /\
   (GF256_by_14 0x1Cw = 0xA8w) /\
   (GF256_by_14 0x1Dw = 0xA6w) /\
   (GF256_by_14 0x1Ew = 0xB4w) /\
   (GF256_by_14 0x1Fw = 0xBAw) /\
   (GF256_by_14 0x20w = 0xDBw) /\
   (GF256_by_14 0x21w = 0xD5w) /\
   (GF256_by_14 0x22w = 0xC7w) /\
   (GF256_by_14 0x23w = 0xC9w) /\
   (GF256_by_14 0x24w = 0xE3w) /\
   (GF256_by_14 0x25w = 0xEDw) /\
   (GF256_by_14 0x26w = 0xFFw) /\
   (GF256_by_14 0x27w = 0xF1w) /\
   (GF256_by_14 0x28w = 0xABw) /\
   (GF256_by_14 0x29w = 0xA5w) /\
   (GF256_by_14 0x2Aw = 0xB7w) /\
   (GF256_by_14 0x2Bw = 0xB9w) /\
   (GF256_by_14 0x2Cw = 0x93w) /\
   (GF256_by_14 0x2Dw = 0x9Dw) /\
   (GF256_by_14 0x2Ew = 0x8Fw) /\
   (GF256_by_14 0x2Fw = 0x81w) /\
   (GF256_by_14 0x30w = 0x3Bw) /\
   (GF256_by_14 0x31w = 0x35w) /\
   (GF256_by_14 0x32w = 0x27w) /\
   (GF256_by_14 0x33w = 0x29w) /\
   (GF256_by_14 0x34w = 0x3w)  /\
   (GF256_by_14 0x35w = 0xDw)  /\
   (GF256_by_14 0x36w = 0x1Fw) /\
   (GF256_by_14 0x37w = 0x11w) /\
   (GF256_by_14 0x38w = 0x4Bw) /\
   (GF256_by_14 0x39w = 0x45w) /\
   (GF256_by_14 0x3Aw = 0x57w) /\
   (GF256_by_14 0x3Bw = 0x59w) /\
   (GF256_by_14 0x3Cw = 0x73w) /\
   (GF256_by_14 0x3Dw = 0x7Dw) /\
   (GF256_by_14 0x3Ew = 0x6Fw) /\
   (GF256_by_14 0x3Fw = 0x61w) /\
   (GF256_by_14 0x40w = 0xADw) /\
   (GF256_by_14 0x41w = 0xA3w) /\
   (GF256_by_14 0x42w = 0xB1w) /\
   (GF256_by_14 0x43w = 0xBFw) /\
   (GF256_by_14 0x44w = 0x95w) /\
   (GF256_by_14 0x45w = 0x9Bw) /\
   (GF256_by_14 0x46w = 0x89w) /\
   (GF256_by_14 0x47w = 0x87w) /\
   (GF256_by_14 0x48w = 0xDDw) /\
   (GF256_by_14 0x49w = 0xD3w) /\
   (GF256_by_14 0x4Aw = 0xC1w) /\
   (GF256_by_14 0x4Bw = 0xCFw) /\
   (GF256_by_14 0x4Cw = 0xE5w) /\
   (GF256_by_14 0x4Dw = 0xEBw) /\
   (GF256_by_14 0x4Ew = 0xF9w) /\
   (GF256_by_14 0x4Fw = 0xF7w) /\
   (GF256_by_14 0x50w = 0x4Dw) /\
   (GF256_by_14 0x51w = 0x43w) /\
   (GF256_by_14 0x52w = 0x51w) /\
   (GF256_by_14 0x53w = 0x5Fw) /\
   (GF256_by_14 0x54w = 0x75w) /\
   (GF256_by_14 0x55w = 0x7Bw) /\
   (GF256_by_14 0x56w = 0x69w) /\
   (GF256_by_14 0x57w = 0x67w) /\
   (GF256_by_14 0x58w = 0x3Dw) /\
   (GF256_by_14 0x59w = 0x33w) /\
   (GF256_by_14 0x5Aw = 0x21w) /\
   (GF256_by_14 0x5Bw = 0x2Fw) /\
   (GF256_by_14 0x5Cw = 0x5w)  /\
   (GF256_by_14 0x5Dw = 0xBw)  /\
   (GF256_by_14 0x5Ew = 0x19w) /\
   (GF256_by_14 0x5Fw = 0x17w) /\
   (GF256_by_14 0x60w = 0x76w) /\
   (GF256_by_14 0x61w = 0x78w) /\
   (GF256_by_14 0x62w = 0x6Aw) /\
   (GF256_by_14 0x63w = 0x64w) /\
   (GF256_by_14 0x64w = 0x4Ew) /\
   (GF256_by_14 0x65w = 0x40w) /\
   (GF256_by_14 0x66w = 0x52w) /\
   (GF256_by_14 0x67w = 0x5Cw) /\
   (GF256_by_14 0x68w = 0x6w)  /\
   (GF256_by_14 0x69w = 0x8w)  /\
   (GF256_by_14 0x6Aw = 0x1Aw) /\
   (GF256_by_14 0x6Bw = 0x14w) /\
   (GF256_by_14 0x6Cw = 0x3Ew) /\
   (GF256_by_14 0x6Dw = 0x30w) /\
   (GF256_by_14 0x6Ew = 0x22w) /\
   (GF256_by_14 0x6Fw = 0x2Cw) /\
   (GF256_by_14 0x70w = 0x96w) /\
   (GF256_by_14 0x71w = 0x98w) /\
   (GF256_by_14 0x72w = 0x8Aw) /\
   (GF256_by_14 0x73w = 0x84w) /\
   (GF256_by_14 0x74w = 0xAEw) /\
   (GF256_by_14 0x75w = 0xA0w) /\
   (GF256_by_14 0x76w = 0xB2w) /\
   (GF256_by_14 0x77w = 0xBCw) /\
   (GF256_by_14 0x78w = 0xE6w) /\
   (GF256_by_14 0x79w = 0xE8w) /\
   (GF256_by_14 0x7Aw = 0xFAw) /\
   (GF256_by_14 0x7Bw = 0xF4w) /\
   (GF256_by_14 0x7Cw = 0xDEw) /\
   (GF256_by_14 0x7Dw = 0xD0w) /\
   (GF256_by_14 0x7Ew = 0xC2w) /\
   (GF256_by_14 0x7Fw = 0xCCw) /\
   (GF256_by_14 0x80w = 0x41w) /\
   (GF256_by_14 0x81w = 0x4Fw) /\
   (GF256_by_14 0x82w = 0x5Dw) /\
   (GF256_by_14 0x83w = 0x53w) /\
   (GF256_by_14 0x84w = 0x79w) /\
   (GF256_by_14 0x85w = 0x77w) /\
   (GF256_by_14 0x86w = 0x65w) /\
   (GF256_by_14 0x87w = 0x6Bw) /\
   (GF256_by_14 0x88w = 0x31w) /\
   (GF256_by_14 0x89w = 0x3Fw) /\
   (GF256_by_14 0x8Aw = 0x2Dw) /\
   (GF256_by_14 0x8Bw = 0x23w) /\
   (GF256_by_14 0x8Cw = 0x9w)  /\
   (GF256_by_14 0x8Dw = 0x7w)  /\
   (GF256_by_14 0x8Ew = 0x15w) /\
   (GF256_by_14 0x8Fw = 0x1Bw) /\
   (GF256_by_14 0x90w = 0xA1w) /\
   (GF256_by_14 0x91w = 0xAFw) /\
   (GF256_by_14 0x92w = 0xBDw) /\
   (GF256_by_14 0x93w = 0xB3w) /\
   (GF256_by_14 0x94w = 0x99w) /\
   (GF256_by_14 0x95w = 0x97w) /\
   (GF256_by_14 0x96w = 0x85w) /\
   (GF256_by_14 0x97w = 0x8Bw) /\
   (GF256_by_14 0x98w = 0xD1w) /\
   (GF256_by_14 0x99w = 0xDFw) /\
   (GF256_by_14 0x9Aw = 0xCDw) /\
   (GF256_by_14 0x9Bw = 0xC3w) /\
   (GF256_by_14 0x9Cw = 0xE9w) /\
   (GF256_by_14 0x9Dw = 0xE7w) /\
   (GF256_by_14 0x9Ew = 0xF5w) /\
   (GF256_by_14 0x9Fw = 0xFBw) /\
   (GF256_by_14 0xA0w = 0x9Aw) /\
   (GF256_by_14 0xA1w = 0x94w) /\
   (GF256_by_14 0xA2w = 0x86w) /\
   (GF256_by_14 0xA3w = 0x88w) /\
   (GF256_by_14 0xA4w = 0xA2w) /\
   (GF256_by_14 0xA5w = 0xACw) /\
   (GF256_by_14 0xA6w = 0xBEw) /\
   (GF256_by_14 0xA7w = 0xB0w) /\
   (GF256_by_14 0xA8w = 0xEAw) /\
   (GF256_by_14 0xA9w = 0xE4w) /\
   (GF256_by_14 0xAAw = 0xF6w) /\
   (GF256_by_14 0xABw = 0xF8w) /\
   (GF256_by_14 0xACw = 0xD2w) /\
   (GF256_by_14 0xADw = 0xDCw) /\
   (GF256_by_14 0xAEw = 0xCEw) /\
   (GF256_by_14 0xAFw = 0xC0w) /\
   (GF256_by_14 0xB0w = 0x7Aw) /\
   (GF256_by_14 0xB1w = 0x74w) /\
   (GF256_by_14 0xB2w = 0x66w) /\
   (GF256_by_14 0xB3w = 0x68w) /\
   (GF256_by_14 0xB4w = 0x42w) /\
   (GF256_by_14 0xB5w = 0x4Cw) /\
   (GF256_by_14 0xB6w = 0x5Ew) /\
   (GF256_by_14 0xB7w = 0x50w) /\
   (GF256_by_14 0xB8w = 0xAw)  /\
   (GF256_by_14 0xB9w = 0x4w)  /\
   (GF256_by_14 0xBAw = 0x16w) /\
   (GF256_by_14 0xBBw = 0x18w) /\
   (GF256_by_14 0xBCw = 0x32w) /\
   (GF256_by_14 0xBDw = 0x3Cw) /\
   (GF256_by_14 0xBEw = 0x2Ew) /\
   (GF256_by_14 0xBFw = 0x20w) /\
   (GF256_by_14 0xC0w = 0xECw) /\
   (GF256_by_14 0xC1w = 0xE2w) /\
   (GF256_by_14 0xC2w = 0xF0w) /\
   (GF256_by_14 0xC3w = 0xFEw) /\
   (GF256_by_14 0xC4w = 0xD4w) /\
   (GF256_by_14 0xC5w = 0xDAw) /\
   (GF256_by_14 0xC6w = 0xC8w) /\
   (GF256_by_14 0xC7w = 0xC6w) /\
   (GF256_by_14 0xC8w = 0x9Cw) /\
   (GF256_by_14 0xC9w = 0x92w) /\
   (GF256_by_14 0xCAw = 0x80w) /\
   (GF256_by_14 0xCBw = 0x8Ew) /\
   (GF256_by_14 0xCCw = 0xA4w) /\
   (GF256_by_14 0xCDw = 0xAAw) /\
   (GF256_by_14 0xCEw = 0xB8w) /\
   (GF256_by_14 0xCFw = 0xB6w) /\
   (GF256_by_14 0xD0w = 0xCw)  /\
   (GF256_by_14 0xD1w = 0x2w)  /\
   (GF256_by_14 0xD2w = 0x10w) /\
   (GF256_by_14 0xD3w = 0x1Ew) /\
   (GF256_by_14 0xD4w = 0x34w) /\
   (GF256_by_14 0xD5w = 0x3Aw) /\
   (GF256_by_14 0xD6w = 0x28w) /\
   (GF256_by_14 0xD7w = 0x26w) /\
   (GF256_by_14 0xD8w = 0x7Cw) /\
   (GF256_by_14 0xD9w = 0x72w) /\
   (GF256_by_14 0xDAw = 0x60w) /\
   (GF256_by_14 0xDBw = 0x6Ew) /\
   (GF256_by_14 0xDCw = 0x44w) /\
   (GF256_by_14 0xDDw = 0x4Aw) /\
   (GF256_by_14 0xDEw = 0x58w) /\
   (GF256_by_14 0xDFw = 0x56w) /\
   (GF256_by_14 0xE0w = 0x37w) /\
   (GF256_by_14 0xE1w = 0x39w) /\
   (GF256_by_14 0xE2w = 0x2Bw) /\
   (GF256_by_14 0xE3w = 0x25w) /\
   (GF256_by_14 0xE4w = 0xFw)  /\
   (GF256_by_14 0xE5w = 0x1w)  /\
   (GF256_by_14 0xE6w = 0x13w) /\
   (GF256_by_14 0xE7w = 0x1Dw) /\
   (GF256_by_14 0xE8w = 0x47w) /\
   (GF256_by_14 0xE9w = 0x49w) /\
   (GF256_by_14 0xEAw = 0x5Bw) /\
   (GF256_by_14 0xEBw = 0x55w) /\
   (GF256_by_14 0xECw = 0x7Fw) /\
   (GF256_by_14 0xEDw = 0x71w) /\
   (GF256_by_14 0xEEw = 0x63w) /\
   (GF256_by_14 0xEFw = 0x6Dw) /\
   (GF256_by_14 0xF0w = 0xD7w) /\
   (GF256_by_14 0xF1w = 0xD9w) /\
   (GF256_by_14 0xF2w = 0xCBw) /\
   (GF256_by_14 0xF3w = 0xC5w) /\
   (GF256_by_14 0xF4w = 0xEFw) /\
   (GF256_by_14 0xF5w = 0xE1w) /\
   (GF256_by_14 0xF6w = 0xF3w) /\
   (GF256_by_14 0xF7w = 0xFDw) /\
   (GF256_by_14 0xF8w = 0xA7w) /\
   (GF256_by_14 0xF9w = 0xA9w) /\
   (GF256_by_14 0xFAw = 0xBBw) /\
   (GF256_by_14 0xFBw = 0xB5w) /\
   (GF256_by_14 0xFCw = 0x9Fw) /\
   (GF256_by_14 0xFDw = 0x91w) /\
   (GF256_by_14 0xFEw = 0x83w) /\
   (GF256_by_14 0xFFw = 0x8Dw)`;

*)

val _ = export_theory();
